SIPL library is a collection of Nuprl theories that formalize syntax and semantics of a simple imperative programming language. Syntax and transition semantics are based on those given in C. Gunter book. This library also includes theory of Hoare's predicate and tactic support for proving Hoare's statements about actual programs.

Pavel Naumov (pavel@cs.cornell.edu) 

• expression. Expression is a recursive type built from Z and Atom by operations of addition, multiplication, subtraction, and sign change:

Exp :: =  Z  |  Atom  |  Exp + Exp  |  Exp  * Exp  |  Exp - Exp  |  -Exp

Also we define a map

expval  :  Exp  x  (Atom -> Z)  --> Z

• boolean expression. Boolean expressions are defined as follows:

BExp :: =  Bool  |  BExp and BExp  |  BExp or BExp  | 

 | not BExp  |  Exp < Exp |  Exp = Exp

Where Bool is a standard two-element type. Boolean analog of expval is also defined in this theory:

bexpval : BExp x (Atom -> Z) --> Z

• command. I define commands (statements) of Simple Imperative Programming Language as:

C :: = skip  | C ; C  |  Atom := Exp |  if BExp then C else C fi |

 | while BExp do C od

• transition. In this theory I define transition (re-write) semantics for Simple Imperative Programming Language. The basic notion of this theory is configuration. Configuration is a pair of a command and a memory:

Conf := C x (Atom -> Z)

And the basic function is a function that maps any configuration into the successor:

next : Conf -> Conf

It is not absolutely obvious which configuration I consider the successor. Please, refer to the library for the definition.

If next is already given we can define operator nth as a simple iteration of next:

nth : Conf x Z -> Conf

Finally, configuration cf evolves to memory m if for some natural number n:

nth(cf, n) = <skip, m'>

Reader will find lots of theorems in transition theory. Most of them are proven in order to use in hoare theory. But theorem evolves_inv has independent value - it states that any configuration cannot evolve to more than one final state of memory. Proof of this theorem is rather trivial and is based on the fact that for any mamory m, <skip, m> is a fixed point for operator next.

• hoare. Using transition semantics I prove here the properties of the famous Hoare's predicate. This theory also includes powerful set of tactics to prove Hoare's statement about programs.
• hoare_examples. Collection of Hoare statement proofs for different programs. Includes programs that compute factorial and GCD.

References:

1. Semantics of Programming Languages: Structures and Techniques, Carl A. Gunter, MIT Press, 1992
2. Mathematical Theory of Program Correctness, Jaco de Bakker, Prentice Hall, 1980
3. Procedures and Parameters: An Axiomatic Approach, C.A.R. Hoare, in Lecture Notes in Mathematics 188, Springer, 1971