On the verification of modules

  • G. Antoniou
  • V. Sperschneider
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 440)


We present a module concept with algebraic interface and imperative implementation. It is shown that under some natural conditions, module correctness may be uniformly expressed in Hoare logic as a partial correctness assertion.


Function Symbol Structure Object Relation Symbol Import Term Access Path 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Ant 89]
    Antoniou,G.: Über die Verifikation modularer Programme, Dissertation, Fachbereich Mathematik/Informatik, Universität Osnabrück 1989.Google Scholar
  2. [BEP 87]
    Blum, E.K., Ehrig, H. & Parisi-Presicce, F.: Algebraic Specification of Modules and Their Basic Interconnections, JCSS 34, pp. 293–339, 1987Google Scholar
  3. [EM 85]
    Ehrig,H., Mahr,B.: Fundamentals of Algebraic Specification 1, Springer 1985.Google Scholar
  4. [Hoa 69]
    Hoare, C.A.R.: An axiomatic basis for computer programming, Comm. ACM 12 (1969), 567–580.Google Scholar
  5. [K 83]
    Klaeren,H.A.: Algbraische Spezifikation-Eine Einführung, Springer Lehrbuch Informatik, 1983Google Scholar
  6. [KU 85]
    Kfoury, A.J. & Urzyczyn, P.: Necessary and Sufficient Conditions for the Universality of Programming Formalisms, Acta Informatica 22, pp. 347–377, 1985CrossRefGoogle Scholar
  7. [L 87]
    Loeckx,J.: Algorithmic specifications: a constructive specification method for abstract data types, ACM Transactions on Programming Languages and Systems, 9(4), 1987.Google Scholar
  8. [LS 87]
    Loeckx,J., Sieber,K.: The Foundations of Program Verification, Wiley 1984/87.Google Scholar
  9. [McG 82]
    McGettrick,A.D.: Program Verification using Ada, Cambridge University Press, 1982Google Scholar
  10. [SA 90]
    Sperschneider, V. & Antoniou,G: Logic: A Foundation for Computer Science, Addison-Wesley, to appearGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • G. Antoniou
    • 1
  • V. Sperschneider
    • 1
  1. 1.Universität OsnabrückGermany

Personalised recommendations