DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
Penelope Reference Manual, Version 3-3 (COO 1), includes Larch/Ada Specification Manual for Sequential Ada (C002).
UNISYS CORP RESTON VA RESTON TECHNOLOGY CENTER
Pagination or Media Count:
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 Diijkstra. 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. With Penelope, it is often possible to modify a verified program and verify the modified version with minimal effort by replaying and modifying the original programs proof.
APPROVED FOR PUBLIC RELEASE