Publication Date


Document Type


Committee Members

Thomas C. Hartrum (Committee Co-chair), Mateen M. Rizki (Committee Co-chair), Thomas Sudkamp (Other), Krishnaprasad Thirunarayan (Committee Member), Joseph F. Thomas, Jr. (Other)

Degree Name

Master of Science (MS)


Software engineers have been trying for years to develop a software synthesis system that can transform a formal specification model to a design model from which executable code can be generated. AFIT wide spectrum object modeling environment (AWESOME) is one result of their research. AWESOME presents a formal model as an abstract syntax tree. This model consists mainly of object class specifications. The methods in these classes are specified using pre and post-conditions. The intent of this thesis is to support the transformation of post-conditions to code statements. A post-condition is first categorized as dependent or independent relative to other post-conditions. Post-conditions are further divided into actions and constraints. Actions can be converted to executable statements. Constraints can be converted to pre-conditions using weakest pre-condition analysis. Functions have been designed to categorize the post-conditions. Transforms have been designed to simplify the post-conditions and to determine the weakest pre-condition and add it to the method. The result is a design model from which executable code can be generated.

Page Count


Department or Program

Department of Computer Science

Year Degree Awarded