Simple Imperative Programming
Nuprl 4.2 with sexp_1 theory
- 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.
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
expression. Boolean expressions are
defined as follows:
BExp :: = Bool |
BExp and BExp | BExp or
| 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
I define commands (statements) of Simple Imperative Programming Language
C :: = skip | C ; C
| Atom := Exp | if BExp then
C else C fi |
| while BExp do C
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,
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.
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.
Collection of Hoare statement proofs for different programs. Includes programs
that compute factorial and GCD.
Languages: Structures and Techniques, Carl
A. Gunter, MIT Press,
- Mathematical Theory of Program Correctness,
Jaco de Bakker, Prentice Hall, 1980
- Procedures and Parameters: An Axiomatic
Hoare, in Lecture Notes in Mathematics 188, Springer,