- 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:**boolean expression.**Boolean expressions are defined as follows:**command.**I define commands (statements) of Simple Imperative Programming Language as:**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:**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.

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

Also we define a map

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

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

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

| **while** *BExp* **do** *C*
**od**

*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*.

**References:**

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