=ADD=
=reftype=
14
=number=
99-16
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1999/99-16.ps.gz
=note=
Diploma Thesis, FHS Hagenberg. Also available as Mathematica notebook ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1999/99-16.nb.gz
=year=
1999
=month=
07
=author=
Kirchner; Martin
=title=
Program Verification with the Mathematical Software System Theorema
=abstract=
With Theorema, the Research Institute for Symbolic Computation in
Hagenberg attempts to develop an integrated and comprehensive
mathematical environment, with emphasis on a "natural" mathematical
language with clear semantics and the support of mathematical proving.
Within the scope of the thesis we have extended Theorema by a
verification system for simple sequential programs.
The verification system is designed for educational purposes. It
provides an environment for Software Engineering students to learn the
basics of formal methods in software development: the formal
specification of programs, the annotation of programs and the formal
proof of correctness.
The most important part of the verification system is a tool, which
takes a specification and an annotated program and generates
so-called verification conditions. These are mathematical
statements which are to be proved; either by "hand", using an existing
automated Theorema prover, or with an interactive interface to a
Theorema prover. In the thesis we discuss the implementation of such a
verification condition generator based on a "predicate transformer"
function, and describe the verification rules in  detail.
The user interfaces for specifications and programs follow the
conventions of Theorema and are also presented elaborately. The programs
to verify are written in Theorema Procedural Language, a small language
designed in the scope of this thesis to enable procedural programming
within the functional environment of Theorema. The embedding of this
language into the Theorema system allows to specify, implement, verify
and execute programs within one uniform environment. We demonstrate the
use of the system in numerous examples and provide a tutorial for future
users.
=keywords=
program verification, verification condition generator, mathematical education
=end=