The Development of a Graphical Notation for the Formal Specification of Software
AIR FORCE INST OF TECH WRIGHT-PATTERSON AFB OH SCHOOL OF ENGINEERING
Pagination or Media Count:
The program tranformations lifecycle model, proposed by Balzer in 1984, may hold the key to dramatic leap in software engineer productivity necessitated by the tremendous growth in the worlds demand for software. This leap in productivity is made possible by the program transformation lifecycles reliance on formal specifications rather than programs as the primary vehicle for the creation and maintenance of software systems. Because formal specifications are concerned only with system behaviors and not implementation details, formal specifications tend to present critical system characteristics much more concisely than programs. The major disadvantage of using formal specifications in a software development process, however, is that, because of their highly mathematical nature, formal specifications tend to be very difficult to create, understand, and maintain for the average software engineer or programmer. This thesis develops a graphical formal specification language based on the Refine wide spectrum language using a graph based iconic representation to present formal specifications in a format that is much easier to create and manipulate than the equivalent textual formal specifications.
- Computer Programming and Software