ANALYSIS AND TRANSFORMATION OF POST-CONDITIONS

by VASIKARLA, ABHINAV

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.