Specifications & Proof Scores
Prolog
Specifications
Semantics of the IMP language
Semantics of the IMP language with the 'mod' operator
Semantics of the IMP language with variable declarations
Semantics of the IMP language with a simple type system
Semantics of the IMP language with blocks, local declarations, and I/O
Semantics of the IMP language with function calls
Translation specifcation
Translation specifcations all contained in a zip file
sans aexp correctness proof.
List language specifcation and examples all contained in a zip file
Proof Scores
standard proof pramble, sets up standard proof score environment.
Extended is predicate - now version 4!
simple semantic proof
prove that mult(2,3) ~ add(3,3)
prove that add(a0,a1) ~ add(a1,a0)
prove that true ~ not(false)
prove the execution of a program
prove that assign(x,1) seq assign(y,2) ~ assign(y,2) seq assign(x,1)
induction proof on arithmetic expressions
an example that recursion works for function calls
proof that the program P satisfies the swap specification
proof that the program P satisfies the doubling specification
proof that the program P satisfies the swap pre- and postconitions
proof that the program P satisfies the max pre- and postconitions
proof using loop invariants
fact.pl - another proof using loop invariants
correctness proofs of loops and functions