Advertisement

Acta Informatica

, Volume 6, Issue 1, pp 15–40 | Cite as

Specification and proving of command programs

  • E. J. Neuhold
  • T. Weller
Article
  • 26 Downloads

Summary

In this paper a method is described by which command languages can be specified in a precise and comprehensive way and which allows the correctness of command programs to be proven automatically. The described technique is based on an abstract command processor (ACP) which was developed both from principles of abstract interpreters and of axiomatic definitions.

A formal description of a sample command language (SCL) is given by identifying in an axiomatic manner the set of ACP state transformations arising during the execution of the commands and by defining interpretatively which of these transformations are chosen in a given context. Using this definition the correctness of a command program can be proven in a nonheuristic manner. The technique is demonstrated on a SCL example.

Keywords

Information System Operating System Data Structure Communication Network Information Theory 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bandat, K.: Semantik von Betriebssystemen (Semantics of Operating Systems). NTG-Fachtagung über Betriebssysteme, Darmstadt, 1972. Berlin: VDE-Verlag, 1972, p. 106–115Google Scholar
  2. 2.
    See for example the review article: Elspas, B., Levitt, K., Waldinger, R., Waksman, A.: An assessment of techniques for proving program correctness. Computing Surveys 4, 97–147 (1972)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.): Mathematical aspects of computer science 19. Providence (R.I.): Amer. Math. Soc., 1967, p. 19–32CrossRefGoogle Scholar
  4. 4.
    Hoare, C.A.R., Wirth, N.: An axiomatic definition of the programming language Pascal. Acta Informatica 2, 335–355 (1973)CrossRefGoogle Scholar
  5. 5.
    King, J.C.: A new approach to program testing. Proceedings of the Int. ACM Conference on Reliable Software, Los Angeles, 1975, p. 228–233Google Scholar
  6. 6.
    Lee, J.A.N.: Computer semantics. London: van Nostrand Reinhold 1972Google Scholar
  7. 7.
    Lucas, P., Walk, K.: On the formal description of PL/I. Annual Review in Automatic Programming 6, 105–182 (1969)CrossRefGoogle Scholar
  8. 8.
    Neuhold, E. J.: The formal description of programming languages. IBM Systems Journal 10, 86–112 (1971)CrossRefGoogle Scholar
  9. 9.
    Niggemann, N.: A method for the semantic description of command languages. In: Unger, C. (ed.): Command languages. Proceedings of the IFIP Working Conference on Command Languages 1975. Amsterdam: North-Holland 1975, P. 223–236Google Scholar
  10. 10.
    Remark of T.B. Steel, during the IFIP Working Conference. In: Unger, C. (ed.): Command languages. Proceedings of the IFIP Working Conference on Command Languages 1975. Amsterdam: North-Holland 1975, p. 205Google Scholar
  11. 11.
    Weller, T.: On the user-oriented semantics of command languages. In: Unger, C. (ed.): Command languages. Proceedings of the IFIP Working Conference on Command Languages 1975. Amsterdam: North-Holland 1975, P. 237–246Google Scholar

Copyright information

© Springer-Verlag 1976

Authors and Affiliations

  • E. J. Neuhold
    • 1
  • T. Weller
    • 2
  1. 1.Institut für InformatikUniversität StuttgartStuttgartGermany
  2. 2.Philips GmbH Werk für BasiscomputersystemeEiserfeldGermany

Personalised recommendations