This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Trace Specifications: Methodology and Models
September 1988 (vol. 14 no. 9)
pp. 1243-1252

The authors summarize the trace specification language and present the trace specification methodology: a set of heuristics designed to make the reading and writing of complex specifications manageable. Also described is a technique for constructing formal, executable models from specifications written using the methodology. These models are useful as proof of specification consistency and as executable prototypes. Fully worked examples of the methodology and the model building techniques are included.

[1] A. L. Ambler, D. I. Good, J. C. Browne, W. F. Burger, R. M. Cohen, C. G. Hoch, and R. E. Wells, "Gypsy: A language for specification and implementation of verifiable programs," inProc. ACM Conf. Language Design for Reliable Software; inSIGPLAN Notices. vol. 12, no. 3, pp. 1-10, Mar. 1977.
[2] W. Bartussek and D. L. Parnas, "Using assertions about traces to write abstract specifications for software modules," inProc. 2nd Conf. Euro. Cooperation Inform.Berlin, Germany: Springer-Verlag, 1978.
[3] R. S. Boyer and J. S. Moore, "Proving theorems about LISP functions,"J. ACM, vol. 22, no. 1, pp. 129-144, Jan. 1975.
[4] R. M. Burstall and J. A. Goguen, "An informal introduction to specifications using CLEAR," inThe Correctness Problem in Computer Science, vol. 13, New York: Academic, 1981, pp. 185-213.
[5] R. M. Burstall, D. B. MacQueen, and D. T. Sannella, "HOPE: an experimental applicative language," inConf. Rec. 1980 Lisp Conf., Jan. 1980, pp. 136-143.
[6] W. F. Clocksin and C. S. Mellish,Programming in Prolog. New York: Springer-Verlag, 1984.
[7] N. H. Gehani, "Specifications: Formal and informal--A case study, "Software--Practice and Experience, vol. 12, pp. 185-213, Jan. 1982.
[8] J. A. Goguen and J. J. Tardo, "An introduction to OBJ: A language for writing and testing formal algebraic program specifications," inProc. 1976 Int. Conf. Parallel Processing, IEEE, 1976, pp. 176- 189.
[9] J. Guttag, "Notes on type abstraction,"IEEE Trans. Software Eng., vol. SE-6, no. 1, pp. 13-23, Jan. 1980.
[10] J. V. Guttag and J. J. Horning, "Formal specification as a design tool," inProc. 7th ACM Symp. Principles of Programming Languages, 1980, pp. 251-261.
[11] J. V. Guttag and J. J. Horning, "The algebraic specification of abstract data types,"Acta Inform., vol. 10, no. 1, pp. 27-52, 1978.
[12] J. V. Guttag, E. Horowitz, and D. R. Musser, "Abstract data types and software validation,"Commun. ACM, vol. 21, pp. 1048-1064, Dec. 1978.
[13] D. M. Hoffman, "Trace specification of communications protocols," Ph.D. dissertation, Dep. Comput. Sci., Univ. North Carolina, 1984.
[14] D. M. Hoffman, "The trace specification of communications protocols,"IEEE Trans. Comput., vol. C-34, no. 12, Dec. 1985.
[15] M. E. Majster, "Limits of the 'algebraic' specification of abstract data types,"SIGPLAN Notices, vol. 12, no. 10, pp. 37-42, Oct. 1977.
[16] M. E. Majster, "Comment on a note by J. J. Martin in SIGPLAN Notices, vol. 12, no. 10,"SIGPLAN Notices, vol. 13, no. 1, pp. 22-23, Jan. 1978.
[17] J. J. Martin, "Critique of Mila E. Majster's 'Limits of the algebraic specification of abstract data types,'"SIGPLAN Notices, vol. 12, no. 12, pp. 28-29, Dec. 1977.
[18] J. McLean, "A formal foundation for the abstract specification of software,"J. ACM, vol. 31, no. 3, pp. 600-627, July 1984.
[19] J. M. McLean, D. Weiss, and C. Landwehr, "Executing trace specifications using Prolog," Naval Research Lab., Tech. Rep. 1985.
[20] D. L. Parnas, "The use of precise specifications in the development of software," inProc. IFIP Congress 1977. Amsterdam, The Netherlands: North-Holland, 1977.
[21] D. L. Parnas and P. C. Clements, "A rational design process: How and why to fake it,"IEEE Trans. Software Eng., vol. SE-12, pp. 251-257, Feb. 1986.
[22] C. A. Sunshineet al., "Specification and verification of communication protocols in AFFIRM,"IEEE Trans. Software Eng., vol. SE- 8, no. 5, pp. 460-489, Sept. 1982.
[23] R. Wilensky,LISPcraft. New York: Norton, 1984.

Index Terms:
formal specification; trace specification language; trace specification methodology; specification consistency; executable prototypes; formal specification; specification languages
Citation:
D. Hoffman, R. Snodgrass, "Trace Specifications: Methodology and Models," IEEE Transactions on Software Engineering, vol. 14, no. 9, pp. 1243-1252, Sept. 1988, doi:10.1109/32.6168
Usage of this product signifies your acceptance of the Terms of Use.