TRANSFORMATION OF FORMALLY DEFINED POST-CONDITIONS INTO TARGET LANGUAGE STATEMENTS

by Parvathaneni, Swetha Padma

For years software engineering researchers have been trying to come up with a software synthesis system that can transform a formal specification model into a design model from which executable code can be generated. AFIT Wide Spectrum Object Modeling Environment (AWSOME) is one such formal based software synthesis system. In this system formal specifications written in AWL are parsed into an AST (Abstract Syntax Tree). The intent of this thesis is to demonstrate the transformation of the postconditions of a method into target language statements. The methods in the classes are specified using pre-conditions and post-conditions. Transforms are developed to eliminate any post-condition that has set operators. After removing the post-condition from the method, statements that achieve the desired results specified by the postcondition are added to the method body. The result is a design model from which executable code can be generated.