Skip to main content
SpringerLink
Log in

Assertion programming

  • Invited Lectures
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1979 (MFCS 1979)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 74))

Abstract

The paper describes a method of the systematic development of programs supplemented by specifications. A program in our sense consists of an instruction (the virtual program) plus the specification which in turn consists of a precondition, a postcondition and a set of assertions. Such a program is called correct if the instruction is totally correct wrt the pre- and postcondition, if it does not abort and if the set of assertions is adequate for the corresponding proof of correctness. In the presented method correct programs are developed by sound transformations. The method is illustrated by the derivation of a bubblesort program.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Back, R. J., On the correctness of refinement steps in program development, Dept. of Computer Science, University of Helsinki, Report A-1978-4.

    Google Scholar 

  2. Bär, D., A Methodology for simultaneously developing and verifying PASCAL programs, in: Constructing Quality Software (Proc. IFIP TC-2 Working Conf., May 1977, Novosibirsk), North Holland, Amsterdam 1978.

    Google Scholar 

  3. Bjørner, D., The Vienna development method (VDM): Software specification & program synthesis, in: Mathematical Studies of Information Processing (Proc. Int. Conf. Kyoto, August 1978), 307–340, to appear in LNCS by Springer Verlag.

    Google Scholar 

  4. Blikle, A., A mathematical approach to the derivation of correct programs, in: Semantics of Programming Languages (Proc. Int. Workshop, Bad Honnef, March 1977), Abteilung Informatik, Universität Dortmund, Bericht Nr. 4,1 (1977), 25–29.

    Google Scholar 

  5. Blikle, A., Towards mathematical structured programming, in: Formal Description of Programming Concepts (Proc. IFIP Working Conf. St. Anarews, N.B. Canada, August 1–5, 1977, E.J. Neuhold, ed.), 183–202, North Holland, Amsterdam 1978.

    Google Scholar 

  6. Blikle, A., A comparative review of some program-verification methods. Mathematical Foundations of Computer Science 1977 (Proc. 6th Symp. Tatranska Lomnica, 1977), Lecture Notes in Computer Science 53, Springer Verlag, Heidelberg 1977, 17–33.

    Google Scholar 

  7. Blikle, A., Specified programming, in: Mathematical Studies of Information Processing (Proc. Int. Conf. Kyoto, August 1978).

    Google Scholar 

  8. Blikle, A., A survey of input-output semantics and program verification. ICS PAS Reports 344 (1979).

    Google Scholar 

  9. Blikle, A., On the development of correct programs with the documentation, College of Eng., University of California, Berkeley, Memo UCB/ERL, M7925, April 1979.

    Google Scholar 

  10. Burstall, R.M. and Darlington, J., A transformation system for developing recursive programs, J. ACM, 24 (1977), 44–67.

    Article  Google Scholar 

  11. Darlington, J., Applications of program transformation to program synthesis, Proc. Symp. of Proving and Improving Programs, Arc-et-Senans 1975, pp. 133–144.

    Google Scholar 

  12. Darlington, J., Transforming specifications into efficient programs. New Directions in Algorithmic Languages 1976 (ed. S.A. Schuman), IRIA Rocquencourt 1976.

    Google Scholar 

  13. Dershowitz, N. and Manna, Z., Inference rules for program annotation, Report No. STAN-CS-77-631 (1977).

    Google Scholar 

  14. Dijkstra, E.W., A constructive approach to the problem of program correctness, BIT 8 (1968), 174–186.

    Google Scholar 

  15. Dijkstra, E.W., Guarded commands, non-determinism and a calculus for the derivation of programs, Proc. 1975 Int. Conf. Reliable Software, pp. 2.0–2.13. Also in: Comm. ACM, 18 (1975), 453–457.

    Google Scholar 

  16. Dijkstra, E.W., Formal techniques and sizable programs, Proc. 1st Conf. Eur. Coop. Inf. Amsterdam 1976, Lecture Notes Comput. Sci. 44, 225–235 (1976).

    Google Scholar 

  17. Emden van, M.H., Verification conditions as representations for programs, manuscript (1975).

    Google Scholar 

  18. Emden van, M.H., Unstructured systematic programming, Dept. CS, Univ. Waterloo, CS-76-09 (1976).

    Google Scholar 

  19. Erig, H., Kreowski, H.J., Padawitz, P., Stepwise specification and implementation of abstract data types, in: Automata Languages and Programming (Proc. Fifth Coll. Udine, July 1978), Springer-Verlag LNCS 62, New York 1978, 205–226.

    Google Scholar 

  20. Floyd, R.W., Assigning meanings to programs, Proc. Sym. in Applied Math., 19 (1967), 19–32.

    Google Scholar 

  21. Goguen, J., Some ideas in algebraic semantics, (manuscript) presented at IBM Conference in Kyoto (Japan), 1978.

    Google Scholar 

  22. Goguen, J.A., Thatcher, J.W., Wagner, E.G., Wright, J.B., Abstract data types as initial algebras and correctness of data representations, Proc. Conf. on Comp. Graphics, Pattern Recognition and Data Structure, May 1975, 89–93.

    Google Scholar 

  23. Guttag, J., Abstract data types and the development of data structures, Comm. ACM, 20 (1977), 396–404.

    Article  Google Scholar 

  24. Irlik, J., Constructing iterative version of a system of recursive procedures, In: MFCS (Proc. Int. Symp. MFCS'76) Lecture Notes in CS, Springer-Verlag, Heidelberg 1976, vol. 45.

    Google Scholar 

  25. Lee, S., de Roever, W.R., Gerhart, S.L., The evolution of list-copying algorithms, 6th ACM Symposium on Principles of Programming Languages, January 1979.

    Google Scholar 

  26. Liskov, B.H., Zilles, S.N., Specification techniques for data abstraction, IEEE Trans. on SE Vol. Se-1, No. 1 (1975), 7–19.

    Google Scholar 

  27. Manna, Z., Mathematical Theory of Computation, McGraw-Hill, New York 1974.

    Google Scholar 

  28. Manna, Z., Pnueli, A., Axiomatic approach to total correctness of programs, Acta Informatica (1974).

    Google Scholar 

  29. McCarthy, J., A basis for a mathematical theory of computation, in: Computer Programming and Formal Systems, R. Braffort and D. Hirschberg eds., North-Holland, Amsterdam 1976, pp. 33–70.

    Google Scholar 

  30. Spitzen, J.M., Levitt, K.N., Lawrence, R., An example of hierarchial design and proof. New Directions in Algorithmic Languages 1976 (ed. S.A. Schuman), IRIA, Rocquencourt 1976.

    Google Scholar 

  31. Wegbreit, B., Goal-directed program transformations, IEEE TSE. Vol. SE-2, No. 2, (1976), 69–79.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Polish Academy of Sciences, PKiN, P.O. Box 22, 00-901, Warsaw, Poland

    Andrzej J. Blikle

Authors
  1. Andrzej J. Blikle
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jiří Bečvář

Rights and permissions

Reprints and permissions

Copyright information

© 1979 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Blikle, A.J. (1979). Assertion programming. In: Bečvář, J. (eds) Mathematical Foundations of Computer Science 1979. MFCS 1979. Lecture Notes in Computer Science, vol 74. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-09526-8_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-09526-8_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-09526-2

  • Online ISBN: 978-3-540-35088-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation