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
FPP can do several things for you:
X := X+1; --!Post: X > 0; will give the result: --> wp : (x + 1) > 0;
--!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;
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.
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.
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
Home | Comments | Stefan Kauer 1996.10.10 | Jürgen Winkler 2008May27