Formal models of stepwise refinements of programs

ABSTRACT

Of the many ways to express program specifications, three of the most common are: as a pair of assertions, an input assertion and an output assertion; as a function mapping legal inputs to correct outputs; or as a relation containing the input/output pairs that are considered correct. The construction of programs consists of mapping a potentially complex specification into a program by recursively decomposing complex specifications into simpler ones. We show how this decomposition takes place in all three modes of specification and draw some conclusions on the nature of programming.

REFERENCES

• 1: BARSTOW, D. R. 1979. Knowledge Based Program Construction. North-Holland, Amsterdam, 1979.
• 2: David R. Barstow, Domain-specific automatic programming, IEEE Transactions on Software Engineering, v.11 n.11, p.1321-1336, Nov. 1985 [doi>10.1109/TSE.1985.231881]
• 3: BASILI, V. R., AND NOONAN, R. E. 1980. A comparison of the axiomatic and functional models of structured programming. IEEE Trans. Softw. Eng. SE-6, 5, 454-465.
• 4: BASU, S. K., AND MISRA, j. D. 1975. Proving loop programs. IEEE Trans. Softw. Eng. SE-1, 1, 76-86.
• 5: Per Brinch Hansen, The Architecture of Concurrent Programs, Prentice Hall PTR, Upper Saddle River, NJ, 1977
• 6: Samuel Daniel Conte , Carl W. De Boor, Elementary Numerical Analysis: An Algorithmic Approach, McGraw-Hill Higher Education, 1980
• 7: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 8: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 9: Douglas D. Dunlop , Victor R. Basili, A Comparative Analysis of Functional Correctness, ACM Computing Surveys (CSUR), v.14 n.2, p.229-244, June 1982 [doi>10.1145/356876.356881]
• 10: FLOYD, R. 1967. Assigning meanings to programs. In Proceedings of the AMS Symposium on Applied Mathematics (Providence, R.I.). American Mathematical Society, Providence, R.I., pp. 19-31.
• 11: GRIES, D. 1980. Educating the programmer: Notations, proofs, and the development of programs. In Proceedings of the {FIP 8th Worm Computer Congress (Tokyo and Melbourne), S. Lavington, Ed. North Holland, Amsterdam, pp. 935-944.
• 12: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 13: J V Guttag , J J Horning, Report on the Larch shared language, Science of Computer Programming, v.6 n.2, p.103-134, March 1986
• 14: J V Guttag , J J Horning, A Larch shared language handbook, Science of Computer Programming, v.6 n.2, p.135-157, March 1986
• 15: GUTTAG, J. V., HORNING, J. J., AND WING, J. M. 1985. The Larch family of specification languages. IEEE Software 2, 5 (Sept.), 24-36.
• 16: Eric C. R. Hehner, Predicative programming Part I, Communications of the ACM, v.27 n.2, p.134-143, Feb. 1984 [doi>10.1145/69610.357988]
• 17: Eric C. R. Hehner, Predicative programming Part II, Communications of the ACM, v.27 n.2, p.144-151, Feb. 1984 [doi>10.1145/69610.357990]
• 18: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 19: IGARASHI, $., LONDON, R. L., AND LUCKHAM, D. C. 1975. Automatic program verification: A logical basis and its implementation. Acta Inform. 4, 145-182.
• 20: Kathleen Jensen , Niklaus Wirth, Pascal-User Manual and Report, Springer-Verlag New York, Inc., Secaucus, NJ, 1975
• 21: Cliff B. Jones, Software Development: A Rigorous Approach, Prentice Hall PTR, Upper Saddle River, NJ, 1980
• 22: Elaine Kant, Understanding and automating algorithm design, IEEE Transactions on Software Engineering, v.11 n.11, p.1361-1374, Nov. 1985 [doi>10.1109/TSE.1985.231884]
• 23: LARSON, L. C. 1983. Problem-Solving through Problems. Springer Publ., New York.
• 24: Richard C. Linger , Bernard I. Witt , H. D. Mills, Structured Programming; Theory and Practice the Systems Programming Series, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1979
• 25: C. L Liu, Elements of discrete mathematics (McGraw-Hill computer science series), McGraw-Hill Pub. Co., 1977
• 26: LIVERCY, C. 1978. Th~orie des Programmes: Schrnas, Preuves, S~mantique. Dunod Informatique, Paris.
• 27: Zohar Manna, Introduction to Mathematical Theory of Computation, McGraw-Hill, Inc., New York, NY, 1974
• 28: Zohar Manna , Richard Waldinger, Studies in Automatic Programming Logic, Elsevier Science Inc., New York, NY, 1977
• 29: MANNA, Z., AND WALDINGER, R. 1978a. The logic of programming. IEEE Trans. Softw. Eng. SE-6, 3, 199-229.
• 30: MANNA, Z., AND WALDINGER, R. 1978b. DEDALUS--The DEDuctive ALgorithm Ur- Synthesizer. In Proceedings of the National Compurer Conference (Anaheim, Calif.), pp. 683-690.
• 31: MEYER, B. 1985. On formalism in specifications. IEEE Software, 2, 1 (Jan.), 6-27.
• 32: MILI, A. 1983. A relational approach to the design of deterministic programs. Acta Inform. 20 (Dec.), 315-329.
• 33: MILI, A. 1985. Une approche relationelle ~ la programmation. Dissertation of Doctorat ~s- Sciences d'Etat, Laboratoire IMAG-INPG, University of Grenoble, Oct. 1985.
• 34: MILLS, H. D. 1972. Mathematical foundations for structured programming. Publ. FSC 72-6012, Federal Systems Division, IBM, Gaithersburg, Md.
• 35: Harlan D. Mills, The new math of computer programming, Communications of the ACM, v.18 n.1, p.43-48, Jan. 1975 [doi>10.1145/360569.360659]
• 36: MILLS, H. D. 1980. Functional semantics for sequential programs. In Proceedings of the IFIP 8th Worm Computer Congress (Tokyo and Melbourne), S. Lavington, Ed. North-Holland, Amsterdam, pp. 935-944.
• 37: Harlan D. Mills, Princples of Computer Programming, Allyn & Bacon, Inc., Needham Heights, MA, 1987
• 38: Robert Milne , C. Strachey, A Theory of Programming Language Semantics, Halsted Press, New York, NY, 1977
• 39: MORRIS, R., AND WEGBREIT, B. 1977. Program roodification by subgoal induction. In Current Trends in Programming Methodology, vol. 2, R. T. Yeh, Ed. Prentice-Hall, Englewood Cliffs, N.J.
• 40: PAGAN, F. 1981. Formal Specification of Programrning Languages. Prentice-Hall, Englewood Cliffs, N.J.
• 41: David Lorge Parnas, A generalized control structure and its formal definition, Communications of the ACM, v.26 n.8, p.572-581, Aug. 1983 [doi>10.1145/358161.358168]
• 42: POLYA, G. 1965. Mathematical Discovery, vol. I. Wiley, New York.
• 43: REM, M. 1985a. Small programming exercises 7. Sci. Comput. Program. 5, 219-229.
• 44: REM, M. 1985b. Small programming exercises 8. Sci. Comput. Program. 5, 309-316.
• 45: John C. Reynolds, The Craft of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 46: ROBILLARD, P. N. 1985. Le Logiciel: De sa conception sa maintenance. Ga~tan et Morin, Chicoutimi, Quebec, Canada.
• 47: John G. Sanderson, Relational Theory of Computing, Springer-Verlag New York, Inc., Secaucus, NJ, 1980
• 48: SCOTT, D., AND STRACHEY, C. 1971. Toward a mathematical semantics for computer languages. Technical monograph PRG-6. Programming Research Group, University of Oxford, Oxford, England.
• 49: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 50: SUPPES, P. 1972. Axiomatic Set Theory. Dover, New York.
• 51: TARSKI, A. 1941. On the calculus of relations. J. Symb. Logic 6, 3 (Sept.), 73-89.
• 52: Richard C. Waters, The programmer's apprentice: a session with KBEmacs, IEEE Transactions on Software Engineering, v.11 n.11, p.1296-1320, Nov. 1985 [doi>10.1109/TSE.1985.231880]
• 53: Niklaus Wirth, Algorithms + Data Structures = Programs, Prentice Hall PTR, Upper Saddle River, NJ, 1978

INDEX TERMS

Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Design, Languages, Theory, Verification