This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Automatic Derivation of Formal Software Specifications from Informal Descriptions
October 1991 (vol. 17 no. 10)
pp. 1126-1142

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.

[1] R. Balzer, N. Goldman, and D. Wile, "Informality in program specifications,"IEEE Trans. Software Eng., vol. SE-4, pp. 94-103, Mar. 1978.
[2] S. Bhansali and M. T. Marandi, "Program synthesis using derivational analogy," Dept. Comput. Sci., Univ. Illinois, Urbana-Champaign, Tech. Rep. 90-1591, 1990.
[3] M. Broy and P. Pepper, "Program development as a formal activity,"IEEE Trans. Software Eng., vol. SE-7, pp. 14-22, Jan. 1981.
[4] F. L. Bauer and M. Broy, "Program construction," inLecture Notes in Computer Science, vol. 69, Berlin-Heidelberg-New York: Springer-Verlag, 1979.
[5] A. J. Czuchry Jr., "Where's the intelligence in the intelligent assistant for requirements analysis? Inference processes in the KBRA," inProc. 2nd Ann. Knowledge-Based Software Assist. Conf. (Rome Air Development Center, Air Force Systems Command, Griffiss AFB, NY), Jan. 1988, pp. 117-137.
[6] J. Darlington, "An experimental program transformation and synthesis system,"Artificial Intell., vol. 16, pp. 1-46, 1981.
[7] G. DeJong, "An approach to learning from observation," inMachine Learning: An Artificial Intelligence Approach, vol. II, R. S. Michalski, J. G. Carbonell, and T. M. Mitchell, Eds. Los Altos, CA: Morgan Kaufmann, 1986, pp. 571-590.
[8] N. Dershowitz, "Program abstraction and instantiation,"ACM Trans. Program. Languages and Syst., vol. 7, no. 3, pp. 446-477, 1985.
[9] G. Dromey,Propram Derivations--The Development of Programs from Specifications(Int. Computer Science Series). Reading, MA: Addison-Wesley, 1989.
[10] B. Falkenhainer, "Learning from physical analogies: a study in analogy and the explanation process," Dept. Comput. Sci., Univ. Illinois, Urbana-Champaign, Dec. 1988.
[11] M. S. Feather, "Constructing specifications by combining parallel elaborations,"IEEE Trans. Software Eng., vol. 15, pp. 198-208, Feb. 1989.
[12] M. S. Feather, "Detecting interference when merging specifications," inProc. 5th Int. Workshop on Software Specification and Design, Apr. 1989, pp. 169-176.
[13] S. Fickas, "Automating analysis: an example," inproc. 4th Int. Workshop on Software Specification and Design, Apr. 1987, pp. 58-67.
[14] S. Fickas, "Automating the specification process," Dept. Comput. and Inform. Sci., Univ. Oregon, Eugene, Tech. Rep. No. CIS-TR-87-05, Dec. 1987.
[15] S. Fickas and P. Nagarajan, "Being suspicious: critiquing problem specifications," inProc. 7th Nat. Conf. on Artificial Intell., 1988, pp. 19-24.
[16] R. Greiner, "Learning by understanding analogies," Dept. Comput. Sci., Stanford Univ., Palo Alto, CA, Sept. 1985.
[17] J. V. Guttag, J. J. Horning, and J. M. Wing, "Larch in five easy pieces," Digital Equipment Corp., Palo Alto, CA, 1985.
[18] E. Horowitz and S. Sahni,Fundamentals of Data Strucrures. Potomac, MD: Comput. Sci. Press, 1976.
[19] W. L. Johnson, "Deriving specifications from requirements," inProc. 10th Int. Conf. on Software Eng. (Singapore), 1988, pp. 428-438.
[20] W. L. Johnson, "Overview of the knowledge-based specification assistant," inProc. 2nd Ann. Knowledge-Based Software Assist. Conf.(Rome Air Development Ctr., Air Force Systems Command, Griffiss AFB, NY), Jan. 1988, pp. 48-79.
[21] W. L. Johnson, "Turning Ideas into Specifications," inProc. 2nd Ann. Knowledge-Based Software Assist. Conf. (Rome Air Development Ctr., Air Force Systems Command, Griffiss AFB, NY), Jan. 1988, pp. 138-153.
[22] W. L. Johnson and E. Soloway, "PROUST: knowledge-based program understanding,"IEEE Trans. Software Eng., vol. SE-11, pp. 267-275, Mar. 1985.
[23] M. T. Keane,Analogical Problem Solving(Ellis Horwood Series in Computer Sci.), Chichester, UK: Ellis Horwood Ltd., 1988.
[24] S. T. Kedar-Cabelli, "Analogy with purpose in legal reasoning from precedents," Lab. for Comput. Sci., Rutgers Univ., New Brunswick, NJ, Tech. Rep. No. LRP-TR-17, July 1984.
[25] S. T. Kedar-Cabelli, "Formulating concepts and analogies according to purpose," Lab. for Comput. Sci., Rutgers Univ., New Brunswick, NJ, May 1988.
[26] B. Liskov and J. Guttag,Abstraction and Specification in Program Development. Cambridge, MA: MIT Press, 1986.
[27] Manna, Z., and R. Waldinger, "A Deductive Approach to Program Synthesis,"Trans. Programming Languages and Systems, Vol. 2, No. 1, Jan. 1980, pp. 90-121.
[28] S. Amarel, "Program synthesis as a theory formation task: problem representations and solution methods," inMachine Learning: An Artificial Intelligence Approach, vol. II, R. S. Michalski, J. G. Carbonell, and T. M. Mitchell, Eds. Los Altos, CA: Morgan Kaufmann, 1986, pp. 499-570.
[29] K. Miriyala and M. T. Harandi, "Analogical approach to specification derivation," inProc. 5th Int. Workshop on Software Specification and Design, May 1989, pp. 203-210.
[30] J. Q. Ning, "A knowledge-based approach to automatic program analysis," Dept. Comput. Sci., Univ. Illinois, Urbana-Champaign, Sept. 1989.
[31] D. A. Plaisted, "Theorem proving with abstraction,"Artificial Intell., vol. 16, no. 1, pp. 47-108, 1981.
[32] H. B. Reubenstein and R. C. Waters, "The requirements apprentice: An initial scenario," inProc. 5th Int. Workshop Software Specification and Design. Washington, DC: IEEE Computer Society Press, May 1989, pp. 211-218.
[33] H. B. Reubenstein and R. C. Waters, "The requirements apprentice: automated assistance for requirements acquisition,"IEEE Trans. Software Eng., to be published.
[34] C. Rich, R. C. Waters, and H. B. Reubenstein, "Toward a requirements apprentice," inProc. 4th Int. Workshop on Software Specification and Design, Apr. 1987, pp. 79-86.
[35] D. R. Smith, "Top-down synthesis of divide-and-conquer algorithms,"Artificial Intell., vol. 27, no. 1, pp. 43-96, Sept. 1985; reprinted inReadings in Artificial Intelligence and Software Engineering, C. Rich and R. Waters, Eds. Los Altos, CA: Morgan Kaufmann, 1986.
[36] J. W. Ulrich and R. Moll, "Program synthesis by analogy," inProc. ACM Symp. on Artificial Intell. and Program. Languages(Rochester, NY), Aug. 1977, pp. 22-28.
[37] R. C. Waters, "The programmer's apprentice: knowledge-based program editing,"IEEE Trans. Software Eng., vol. SE-8, pp. 1-12, Jan. 1982.

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:
K. Miriyala, M.T. Harandi, "Automatic Derivation of Formal Software Specifications from Informal Descriptions," IEEE Transactions on Software Engineering, vol. 17, no. 10, pp. 1126-1142, Oct. 1991, doi:10.1109/32.99198
Usage of this product signifies your acceptance of the Terms of Use.