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.
- Computer Programming and Software