Representation and Refinement of Visual Specifications in Pegasys.
Abstract
This report describes techniques for the representation and refinement of visual specifications in the context of PegaSys (Programming Environment for the Graphical Analysis of SYStems), a system that supports a visual paradigm for the development and explanation of large software designs. Visual specifications are pictorial, mostly non-textual, descriptions of interactions among conceptual entities in a system design. Pictures have a computational meaning that is represented in a formal language, called the 'form calculus'. The form calculus is extensible in that it contains a core set of primitives which can be used to build a variety of abstract design models. Complexity is managed by means of picture hierarchies, whose construction is guided by a precise refinement methodology. The representation and refinement techniques presented have been implemented and all reasoning is fully automatic and efficient. Determining the validity of a picture refinement, for example, involves either the application of a single graph algorithm or the proof of a formula whose predictions range over small, finite sets. Excerpts from a sample session with PegaSys are used to illustrate a hierarchy of visual specifications. Originator-supplied keywords include: Computer programming, Logical representation, Interactive computer graphics, Program design methodology, and Design refinement.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1984
- Accession Number
- ADA148733
Entities
People
- M. S. Moriconi
Organizations
- SRI International