|
PARTIAL CORRECTNESS -- THE SINGLE ASSERTION APPROACH
Ed. Stefan Sokolowski
800
Abstract
The main objective of the project ``Gdansk Development Method'' was to
provide a unified theory of software specification. Out of the
consideration of the ways, in which a piece of code may satisfy a
specification, was born a modification of Hoare logic that has some
advantages over the classical concept. Programs are specified by and
verified against a single formula rather than a pair of pre- and
post-assertions. This volume contains a collection of reports that
investigate the new notion from the point of view of its practical
applicability, logical propertiess, potential for generalizations and
for mechanical proofs. Also, two case studies are included.
|
|
 |
 |
