The specification statement

ABSTRACT

Dijkstra's programming language is extended by specification statements, which specify parts of a program “yet to be developed.” A weakest precondition semantics is given for these statements so that the extended language has a meaning as precise as the original. The goal is to improve the development of programs, making it closer to manipulations within a single calculus. The extension does this by providing one semantic framework for specifications and programs alike: Developments begin with a program (a single specification statement) and end with a program (in the executable language). And the notion of refinement or satisfaction, which normally relates a specification to its possible implementations, is automatically generalized to act between specifications and between programs as well. A surprising consequence of the extension is the appearance of miracles: program fragments that do not satisfy Dijkstra's Law of the Excluded Miracle. Uses for them are suggested.

REFERENCES

• 1: ABR1AL, J.-R. Generalised substitutions. 26 Rue des Plantes, Paris 75014, France, 1987.
• 2: BACK, R.-J. On the correctness of refinement steps in program development. Tech. Rep. A- 1978-4, Dept. of Computer Science, Univ. of Helsinki, Helsinski, 1978.
• 3: BARRINGER, H., CHENG, J. H., AND JONES, C.B. A logic covering undefinedness in program proofs. Acta Inf. 21 (1984), 251-269.
• 4: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 5: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 6: David Gries , Jan Prins, A new notion of encapsulation, Proceedings of the ACM SIGPLAN 85 symposium on Language issues in programming environments, p.131-139, June 25-28, 1985, Seattle, Washington, United States
• 7: Ian Hayes, Specification case studies, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1987
• 8: Eric C.R. Hehner, The logic of programming, Prentice-Hall, Inc., Upper Saddle River, NJ, 1984
• 9: HOARE, C. A. R. Procedures and parameters: An axiomatic approach. In Symposium on Semantics of Algorithmic Languages. Notes in Mathematics 188, E. Engeler, Ed., Springer-Verlag, New York, 1971.
• 10: HOARE, C. A. R., ANO HE, J. The weakest prespecification. Fundamenta lnformaticae IX (1986), 51-84.
• 11: C B Jones, Systematic software development using VDM, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1986
• 12: JOSEPHS, M. B. Formal methods for stepwise refinement in the Z specification language. Programming Research Group, Oxford Univ., 1986.
• 13: Lambert Meertens, Abstracto 84: The next generation, Proceedings of the 1979 annual conference, p.33-39, January 1979 [doi>10.1145/800177.810022]
• 14: Carroll C. Morgan, Data refinement by miracles, Information Processing Letters, v.26 n.5, p.243-246, Jan. 11, 1988 [doi>10.1016/0020-0190(88)90147-0]
• 15: C. Morgan, Procedures, parameters, and abstraction: separate concerns, Science of Computer Programming, v.11 n.1, p.17-27, Oct. 1988 [doi>10.1016/0167-6423(88)90062-7]
• 16: Carroll Morgan , Ken Robinson, Specification statements and refinements, IBM Journal of Research and Development, v.31 n.5, p.546-555, Sept. 1987
• 17: MORGAN, C. C., ANO SUrRIN, B.A. Specification of the UNIX filing system. IEEE Trans. Softw. Eng. SE-IO, 2 (Mar. 1984).
• 18: Joseph M. Morris, A theoretical basis for stepwise refinement and the programming calculus, Science of Computer Programming, v.9 n.3, p.287-306, December 1, 1987 [doi>10.1016/0167-6423(87)90011-6]
• 19: NELSON, G. A generalization of Dijkstra's calculus. Tech. Rep. 16, Digital Systems Research Center, Palo Alto, Calif., Apr. 1987.
• 20: J. M. Spivey, Understanding Z: a specification language and its formal semantics, Cambridge University Press, New York, NY, 1988
• 21: Niklaus Wirth, Programming in MODULA-2 (3rd corrected ed.), Springer-Verlag New York, Inc., New York, NY, 1985

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)
      D.2.2 Design Tools and Techniques
          Subjects: Top-down programming**
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Pre- and post-conditions

General Terms:
Theory, Verification