Report on Logical Foundations for Penelope

This document presents a method, utilizing process logic, to specify and verify concurrent programs.

The Penelope Ada proof editor allows a user to incrementally develop provably correct Ada programs. The current version of the Penelope system is formally based on a predicate transformer semantics for sequential Ada. The purpose of this work is to provide the mathematical foundations for extending Penelope to Ada tasking programs.

Several issues need to be addressed to this end.

• A suitable logical formalism needs to be defined within which it is possible to reason about concurrent programs. In the case of sequential programs first-order logic was sufficient for this purpose.
• A specification and an annotation language must be defined for stating properties of concurrent programs. In the case of sequential programs input/output conditions and loop invariants are used as specifications.
• A method for defining the semantics of Ada needs to be devised. Given a program and a specification, it must be possible to derive conditions under which the program will satisfy it specifications. This step corresponds to the generation of verification conditions in the sequential case.
• An effective proof procedure must be found for showing that the correctness conditions generated for a program are true. If first-order logic is used, then a first-order theorem prover will suffice, in the concurrent case a theorem prover for a richer language will be needed.
• Finally, a new methodology for the systematic development of correct tasking programs needs to be developed. This includes ways to formally express problem specification, to find proper program annotations and so on.

This document addresses primarily the first three questions. While an appropriate notion of proof is formally defined within our mathematical framework, issues of the engineering of a practical theorem prover are not discussed. The use of the new formalism for proving the correctness of tasking programs is demonstrated with several programming examples. But the development of a verification methodology requires more extensive experience.

STARS-AC-A023/005/00  1 June 94  Initial release to the PAL

Approved for public release; Distribution unlimited

This documentation is provided "AS IS" and without any expressed or
implied warranties whatsoever.  No warranties as to performance,
merchantability, or fitness for a particular purpose exist.
The user must assume the entire risk and liability of using this
document.  In no event shall any person or organization of people be
held responsible for any direct, indirect, consequential or
inconsequential damages or lost profits.