University of Jena, Department of Mathematics & Computer Science
Programming Languages and Compilers

Introduction to the Frege Program Prover   (FPP)

What is the Frege Program Prover ?


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.


What can FPP do for you ?


FPP can do several things for you:


How to use FPP

You write your annotated program into the box in the main page of FPP (you can also paste it). After pressing the submit button FPP will (after some while) give you the answer.
 

Supported language constructs (see also syntax):

Arbitrary nesting of the statements is allowed.

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.
 


Limitations

At the time being there are some limitations in FPP:

Logical expressions are not simplified

This means that FPP will give you sometimes rather long expressions in its answer (see e.g. example 6).
In some future version we will include the simplification of expressions.
 

Reaction to program errors

The reaction to program errors is sometimes somewhat poor. FPP more or less assumes that the program is syntactically and semantically (static semantics) correct. In the example
     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.
 

Proof not successful

If a proof succeeds, the verification condition is true. If a proof fails, either the verification condition is false, which means that the system   (program, specification)   is not consistent, or the prover is not able to prove the verification condition (e.g. if it has not enough knowledge).
 

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


References

Dijkstra, Edsger W.; Scholten, Carel S.: Predicate Calculus and Program Semantics.
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 )

                          top of page


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