Issue No. 10 - October (1991 vol. 17)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.99198
<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>
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
M. Harandi and K. Miriyala, "Automatic Derivation of Formal Software Specifications from Informal Descriptions," in IEEE Transactions on Software Engineering, vol. 17, no. , pp. 1126-1142, 1991.