Issue No. 10 - October (1991 vol. 17)

ISSN: 0098-5589

pp: 1126-1142

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.99198

ABSTRACT

<p>SPECIFIER, an interactive system which derives formal specifications of data types and programs from their informal descriptions, is described. The process of deriving formal specifications is viewed as a problem-solving process. The system uses common problem-solving techniques such as schemas, analogy, and difference-based reasoning to derive formal specifications. If an informal description is a commonly occurring operation for which the system has a schema, then the formal specification is derived by instantiating the schema. If there is a no such schema, SPECIFIER tries to find a previously solved problem which is analogous to the current problem. If the problem found is directly analogous to the current problem, it applies an analogy mapping to obtain a formal specification. On the other hand, if the analogy found is only approximate, it solves the directly analogous part of the problem by analogy and performs difference-based reasoning using the remaining (unmatched) parts to transform the formal specification obtained by analogy to a formal specification for the entire original problem.</p>

INDEX TERMS

formal software specifications; interactive system; data types; problem-solving process; common problem-solving techniques; schemas; analogy; difference-based reasoning; informal description; SPECIFIER; previously solved problem; analogy mapping; automatic programming; data structures; formal specification; software tools

CITATION

M.T. Harandi, K. Miriyala, "Automatic Derivation of Formal Software Specifications from Informal Descriptions",

*IEEE Transactions on Software Engineering*, vol. 17, no. , pp. 1126-1142, October 1991, doi:10.1109/32.99198