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