Generating Executable Code from Formal Specifications of Primitive Objects
AIR FORCE INST OF TECH WRIGHT-PATTERSONAFB OH SCHOOL OF ENGINEERING
Pagination or Media Count:
The concept of developing a model for producing compilable and executable code from formal software specifications has long been a goal of software engineers. Previous research at the Air Force Institute of Technology AFIT has been focused on specification and domain analysis. An analysis model is populated using specifications written in Z. Then, a set of preliminary design transforms refines the specification in the analysis model. This research bridges the gap between analysis and design, allowing source code to be produced from formal specifications of primitive objects using transformational programming. The contribution of this thesis is to transform the analysis model for primitive objects into a design model representing the primitive objects, and to produce compilable and executable source code in Ada 95 from the resulting design model.
- Computer Programming and Software