|
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.
I played a bit with the online demo. When I finally managed to get it to accept my code, it managed to prove it correct. Still, I am not sure exactly what meta-functions can be used in the assertions (e.g., sum works).
Posted to Software-Eng by Ehud Lamm on 7/3/02; 3:48:27 AM
|
The Frege Program Prover (FPP)
