In order to prove partial correctness of a program, NPPV expects as input a specification consisting of
If desired, the user may additionally include after any semicolon ``;''an intermediate assertions, i.e. a logical expression that he expects to be true at that point in the program. Annotations appear within comment braces ``{`` and ``}''.
Such an annotated program is entered and edited in NPPV's main window. Syntactical and similar errors are immediately detected with the cursor placed at the offending position and a meaningful error explanation at the bottom of the screen.
Each annotation must be an open formula in an extension of the language over the data type used in the program. Essentially, it must be a Boolean formula, but in addition to the program variables (also called mutable variables) and to the fundamental operations, formulas in annotations may contain extra variables and functions not declared for the data type. Those so called logic variables and Skolem functions may not be read or written by the program. As a convention, NPPV expects logic variables to start with an uppercase letter.
To see the need for this distinction, consider a specification that asks for
a program to exchange the contents of the variables 
and 
. Thus we are
looking for a program C solving the following specification where the logic variables
M and N stand for some arbitrary but fixed values :
If M and N were program variables, then the program
would be a solution. If C was allowed merely to read M and N, then we still would have the unintended solution
Rather we intended to specify a program C which does not contain M or N and which satisfies
We shall never use quantifiers explicitly in our specifications. Existential quantifiers can be eliminated through Skolemizations, universal quantifiers are assumed to bind every free logical variable.