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

Report Date:

1994-09-02

Pagination or Media Count:

155.0

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 programs 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