For the above reasons we have implemented the program verifier NPPV. The acronym stands for ``New Paltz Program Verifier''. This MS-DOS Program presents a user interface familiar from virtually all programming language implementations, collectively termed as ``interactive development environment'' (IDE).
To be specific, the main screen shows an editor window in which the program together with its specification can be edited. A menu bar above the main window provides the most important commands, such as ``edit'', ``prove'' or ``help''. Others lead to further pull-down sub-menus, all in all providing a comfortable proof development environment.