The ITP/ASIP Project
Summary
Based on J. Goguen's seminal
work on algebraic semantics of imperative programs, it aims to provide a
version of the ITP that may be used to formally specified and verified software.
The algebraic semantics of imperative programs is described by:
- specifying a class of abstract machines and
- giving equational axioms which specify the effect of
programs on such machines.
The equational axioms which describe the semantics of
the programming language features are used to prove the
correctness of programs.
Algebraic semantics differs from other approaches to
program specification and verifications in:
- the choice of first order equational logic as a foundation and
- the systematic use of an implemented formal notation to
provide computer support for proofs.
Source code
You can download the ITP/ASIP project's module
from here.
Documentation
You can download the ITP/ASIP project's documentation
from here.
Manuel Clavel
12 April 2005