ASE2 CARD CATALOG ENTRY
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.
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.
Powered by the Generic Web-Based Reuse Library (GWRL)