ASE2 CARD CATALOG ENTRY
Penelope is an interactive environment that helps its user to develop and verify programs written in a rich subset of sequential Ada. Penelope is well-suited to developing programs in the goal-directed style advocated by Gries and Dijkstra. In this style the programmer develops a program from a specification in a way that ensures the program will meet the specification. Of course, Penelope can also be used to verify previously written programs. Sometimes we have to modify a completed program. With Penelope, it is often possible to verify a modified version of a program with minimal effort, by replaying and modifying the original program's proof.
This manual documents the language and commands of the Penelope environment. It is intended for the Penelope user, who desires to write specifications, develop programs, and carry out correctness proofs using Penelope. The user is assumed to be an Ada programmer with a strong mathematical background. A working knowledge of predicate calculus is essential. Even with such a background, the user may require the assistance of a trained mathematician for the more demanding aspects of Penelope, notably providing consistent axiomatic definitions of functions used in the specifications, organizing the proofs of the verification conditions, and proving lemmas needed during the verification. Chapter 2 documents how to get Penelope running. In order to develop and verify programs using Penelope, though, you will need to understand Penelope's approach to formal verification and to simplification and theorem proving.
STARS-AC-A023/004/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)