Accession Number : ADA289828
Title : Penelope Reference Manual, Version 3-3 (COO 1), includes Larch/Ada Specification Manual for Sequential Ada (C002).
Descriptive Note : Technical rept.,
Corporate Author : UNISYS CORP RESTON VA RESTON TECHNOLOGY CENTER
Personal Author(s) : Marceau, Carla
PDF Url : ADA289828
Report Date : 02 SEP 1994
Pagination or Media Count : 155
Abstract : 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 program's proof.
Descriptors : *PROGRAMMING MANUALS, *COMPUTER PROGRAM VERIFICATION, *ADA PROGRAMMING LANGUAGE, SOFTWARE ENGINEERING, ENVIRONMENTS, INTERACTIONS, SPECIFICATIONS, MODIFICATION, SEQUENCES, INSTRUCTIONS, PROGRAMMERS.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE