The Pegasys Environment for Graphical Documentation of Large Programs
Abstract
This is the final report for ONR contract number N00014-86-C-0775. It describes the PegaSys languages, methodology, and techniques for specifying and reasoning about system structures. PegaSys supports both visual and textual specification, where pictures are intuitive representations of logical assertions written in the textual language. To mitigate the problems of scale, the PegaSys methodology supports both horizontal and vertical hierarchies and provides for user-defined abstractions in specifications. Since PegaSys is based on logic, it can reason about designs and programs. For example, it can prove (automatically) that a structural design hierarchy is correct and find (automatically) a conservative approximation of the semantic effects of changes to programs. These advances will allow the PegaSys environment to be considerably more powerful than the CASE tools currently used in industry to develop large software systems. The first part of this report presents a scenario that illustrates the basic ideas behind the PegaSys languages and methodology. The underlying logic is a decidable subset of Ehdm, a state of the art formal specification language developed in the Computer Science Laboratory. The second part of the report presents the details of our technique for deducing the effects of changes to a program. (Changes to a design are not handled.) The new material presented in this report is not implemented in PegaSys at this time.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 18, 1991
- Accession Number
- ADA236557
Entities
People
- Mark Moriconi
Organizations
- SRI International