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