This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Precise Documentation of Well-Structured Programs
December 1994 (vol. 20 no. 12)
pp. 948-976

Describes a new form of program documentation that is precise, systematic and readable. This documentation comprises a set of displays supplemented by a lexicon and an index. Each display presents a program fragment in such a way that its correctness can be examined without looking at any other display. Each display has three parts: (1) the specification of the program presented in the display, (2) the program itself, and (3) the specifications of programs invoked by this program. The displays are intended to be used by software engineers as a reference document during inspection and maintenance. This paper also introduces a specification technique that is a refinement of H.D. Mills's (1975) functional approach to program documentation and verification; programs are specified and described in tabular form.

[1] Dijkstra, E. W., "The Structure of the "THE Multiprogramming System", ACM Symposium on Operating Systems,Communications of the ACM, Vol. 11, No. 5, May 1968, pp.341-346.
[2] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: Prentice-Hall, 1976.
[3] R. W. Floyd, "Assigning meanings to programs,"Proc. Symp. Appl. Math., vol. 19, 1968; also inMathematical Aspects of Computer Science, J. T. Schwartz, Ed. American Mathematical Society, 1967, pp. 19-32.
[4] E. C. R. Hehner, "Predicative programming, Part 1,"Commun. ACM, vol. 27, no. 2, pp. 134-143, Feb. 1984.
[5] K. L. Heninger, J. Kallander, D. L. Parnas, and J. E. Shore, "Software requirements for the A-7E aircraft," U.S. Naval Res. Lab., Washington, DC, NRL Memorandum Rep. 3876, Nov. 1978, p. 523.
[6] K. L. Heninger, "Specifying software requirements for complex systems: New techniques and their application,"IEEE Trans. Software Eng., vol. SE-6, pp. 2-13, Jan. 1980.
[7] C. A. R. Hoare, "An axiomatic basis for computer programming,"Commun. ACM, vol. 12, no. 10, pp. 576-583, 1969.
[8] M. Iglewski, J. Madey, D. L. Parnas and P. C. Kelly, "Documentation paradigms," McMaster Univ., CRL, Telecommun. Res. Inst. of Ontario (TRIO), Hamilton, Ont., Canada, CRL Rep. 270, July 1993, p. 45.
[9] K. Jensen and N. Wirth, "Pascal user manual and report,"Lecture Notes in Computer Science. New York: Springer-Verlag, 1974, vol. 18, 2nd corrected ed., 1976.
[10] C.B. Jones,Systematic Software Development Using VDM, Prentice Hall Int'l, 1986.
[11] N. Leveson, personal communication, Sept. 10, 1994.
[12] M. E. Majster-Cederbaum, "A simple relation between relational and predicate transformer semantics for nondeterministic programs,"Inform. Processing Lett., vol. 11, no. 4-5, Dec. 1980, pp. 190-192.
[13] H. D. Mills, "The new math of computer programming,"CACM, vol. 18, no. 1, pp. 43-48, Jan. 1975.
[14] H. D. Mills, "Function semantics for sequential programs," inProc. IFIP Congr. 1980, North Holland, 1980, pp. 241-250.
[15] D. Peters and D. L. Parnas, "Generating a test oracle from program documentation," inProc. Int. Symp. on Software Testing and Analysis, Aug. 17-19, 1994, pp. 58-65.
[16] D. L. Parnas, "Information distributions aspects of design methodology," inProc. IFIP Congr. '71, Booklet TA-3, 1971, pp. 26-30.
[17] Parnas, D.L. 1972. On the Criteria to be Used in Decomposing Systems into Modules,Communications of the ACM, Vol.15, pp. 1053-1058.
[18] D. L. Parnas, "A generalized control structure and its formal definition,"Commun. ACM, vol. 26, no. 8, Aug. 1983, pp. 527-581.
[19] D. L. Parnas, P. C. Clements, and D. M. Weiss, "The modular structure of complex systems,"IEEE Trans. Software Eng., vol. SE-11, pp. 259-266, March 1985.
[20] D. L. Parnas and W. W. Wadge, "Less restrictive constructs for structured programs," Queen's, C&IS, Kingston, Ont., Canada, Tech. Rep. 86-186, Oct. 1986, p. 16.
[21] D. L. Parnas and Y. Wang, "The trace assertion method of module interface specification," Queen's, C&IS, Telecommun. Res. Inst. of Ontario (TRIO), Kingston, Ont., Canada, Tech. Rep. 89-261, Oct. 1989, p. 39. (Available from McMaster Univ.)
[22] D. L. Parnas, G. J. K. Asmis, and J. Madey, "Assessment of safetycritical software in nuclear power plants,"Nuclear Safety, vol. 32, no. 2, pp. 189-198, 1991.
[23] D. L. Parnas and J. Madey, "Functional documentation for computer systems engineering. (Version 2)," McMaster Univ., CRL, Telecommun. Res. Inst. of Ontario (TRIO), Hamilton, Ont., Canada, CRL Rep. 237, Sept. 1991, p. 14.
[24] D. L. Parnas, "Tabular representation of relations," McMaster Univ., CRL, Telecommun. Res. Inst. of Ontario (TRIO), Hamilton, Ont., Canada; CRL Rep. 260, Oct. 1992, p. 17.
[25] P. F. Sawicki, "Analiza metody SPS(R) weryfikacji programow" (in Polish), ["An analysis of the SPS(R) method of program verification"], M.Sc. Thesis, Warsaw Univ., Inst. of Informatics, 1992, p. 124.
[26] N. Wirth, "Program development by stepwise refinement,"Commun. ACM, vol. 14, no. 4, pp. 221-227, Apr. 1971.
[27] A. J. van Schouwen, "The A-7 requirements model: Re-examination for real-time systems and an application to monitoring systems," Queen's, C&IS, Telecommun. Res. Inst. of Ontario (TRIO), Kingston, Ont., Canada, Tech. Rep. 90-27, May 1990, p. 93. (Available from McMaster Univ.)
[28] A. J. van Schouwen, D. L. Parnas, and Madey, "Documentation of requirements for computer systems," presented atRE '93 IEEE Int. Symp. on Requirements Eng., San Diego, CA, Jan. 4-6, 1993.

Index Terms:
structured programming; system documentation; program verification; formal specification; software maintenance; precise documentation; well-structured programs; displays; lexicon; index; program fragments; program correctness; specification; software engineering; reference document; software inspection; software maintenance; functional approach; program documentation; program verification; tabular form
Citation:
D. Lorge Parnas, J. Madey, M. Iglewski, "Precise Documentation of Well-Structured Programs," IEEE Transactions on Software Engineering, vol. 20, no. 12, pp. 948-976, Dec. 1994, doi:10.1109/32.368133
Usage of this product signifies your acceptance of the Terms of Use.