Introduction to the Frege Program Prover   (FPP)

The Frege Program Prover (FPP) is an experimental system which performs correctness proofs for simple annotated programs.

The programs can be formulated in a small subset of Ada (see syntax). The annotations are preconditions, postconditions, loop invariants, and termination functions for loops. The correctness proofs are based on the weakest precondition approach and other proof rules as described in the Literature.

FPP can do several things for you:

• compute a weakest precondition for a given statement or statement sequence and a given postcondition, e.g.:

        X := X+1;
        --!Post:  X > 0;

will give the result:

        --> wp : (x + 1) > 0;

• prove whether a program Prog and a specification which consists of a preconditon Pre and a postcondition Post are consistent ; i.e. FPP tries to prove the implication:

Pre => wp(Prog, Post). E.g.:

        --!Pre: X = 0 Or X = 1;
        X := X+1;
        --!Post:  X > 1;

will give the result:

        --> wp       : (1 + x >= 2) 
        --> vc       : (x = 0 OR x = 1 ==> 1 + x >= 2) 
                                 -- "vc" stands for "verification condition"
        --> Result: not proved 
        --> Incorrectness condition: (x = 0 AND 1 - x >= 1)

because X=0 Or X=1 does not imply X>0. In such cases the Incorrectness condition tries to give the user a hint, which initial variable assignment causes the program to be incorrect. On the other hand,

        --!Pre: X = 1;
        X := X+1;
        --!Post:  X > 1;

will give the result:

        --> wp : (x + 1) > 1;
        --> vc : [(x = 1) => ((x + 1) > 1)];
        --> result: proved

In such cases a real (mathematical) proof is performed using an extended version of Analytica (by E.M. Clarke of Carnegie Mellon University, Pittsburgh; 440 kB ps file). You can also find more elaborate examples.
• You can also use FPP as a theorem prover by giving it the following input:

        --!Pre: true;
        NULL;
        --!Post: <theorem to be proved>;

e.g.

        --!Pre: true;
        NULL;
        --!Post: a > b AND b > c => a > c;

which will give the answer:

     --!pre : true; 
     --> wp : a > b AND b > c => a > c; 
     --> vc : [(true) => (a > b AND b > c => a > c)]; 
     --> result: proved 
     NULL; 
     --!post : a > b AND b > c => a > c;

Supported language constructs (see also syntax):

• NULL statement
• assignment statement
• if statement
• case statement
• for statement
• while statement
• sequence of statements
• pre-, post-condition  (Ada Boolean expression)
• loop invariant  (Ada Boolean expression)
• termination function  (Ada arithmetic expression)

The quantifiers FORALL and EXISTS can also be used in Boolean expressions.

You will have observed that the list above does not mention any declarations. At the time being FPP assumes that the identifiers are of type "integer" or of type "Boolean". Therefore, no conditions for type checks are generated.
 

Logical expressions are not simplified

Reaction to program errors

     IF a+1
     THEN a :=0;
     ELSE a := b;
     END IF;
     --!Post: true;

Proof not successful

The underline character  '_'  must not be used in identifiers and numbers

References

Gries, David: The Science of Programming.
Springer, New York etc., 1983. 3-540-90641-X

Winkler, Jürgen F. H.: wp is Basically a State Set Transformer.
Internal Paper, Friedrich-Schiller-University, 1995.Aug

Winkler, Jürgen F. H.: The Frege Program Prover.
42. Intern. Wiss. Kolloquium, Ilmenau, Band 1, pp. 116..121. ISSN 0943-7207 ( pdf )

Freining, Carsten; Kauer, Stefan, Winkler, Jürgen F. H.: Ein Vergleich der Programmbeweiser FPP, NPPV und Spark.
in: Winkler, J. F. H.; Dencker, P.; Keller, H. B.; Tonndorf, M. (Hrsg.): Ada Deutschland Tagung 2002, 127..145.
ISBN 3-8265-9956-X,  ISSN 1433-9986 ( pdf )

                          top of page