Representation and Refinement of Visual Specifications in Pegasys.
Final technical rept. May 81-Feb 84,
SRI INTERNATIONAL MENLO PARK CA COMPUTER SCIENCE LAB
Pagination or Media Count:
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.
- Computer Programming and Software
- Human Factors Engineering and Man Machine Systems