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;

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: provedIn 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.

--!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;

- 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.

In some future version we will include the simplification of expressions.

IF a+1 THEN a :=0; ELSE a := b; END IF; --!Post: true;no error is observed and therefore a somewhat meaningless precondition is computed.

Springer, New York etc.,1990. 3-540-96957-8

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 )

Home | Comments | Stefan Kauer 1996.10.10 | Jürgen Winkler 2008May27