Abstract
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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Antoniou,G.: Über die Verifikation modularer Programme, Dissertation, Fachbereich Mathematik/Informatik, Universität Osnabrück 1989.
Blum, E.K., Ehrig, H. & Parisi-Presicce, F.: Algebraic Specification of Modules and Their Basic Interconnections, JCSS 34, pp. 293–339, 1987
Ehrig,H., Mahr,B.: Fundamentals of Algebraic Specification 1, Springer 1985.
Hoare, C.A.R.: An axiomatic basis for computer programming, Comm. ACM 12 (1969), 567–580.
Klaeren,H.A.: Algbraische Spezifikation-Eine Einführung, Springer Lehrbuch Informatik, 1983
Kfoury, A.J. & Urzyczyn, P.: Necessary and Sufficient Conditions for the Universality of Programming Formalisms, Acta Informatica 22, pp. 347–377, 1985
Loeckx,J.: Algorithmic specifications: a constructive specification method for abstract data types, ACM Transactions on Programming Languages and Systems, 9(4), 1987.
Loeckx,J., Sieber,K.: The Foundations of Program Verification, Wiley 1984/87.
McGettrick,A.D.: Program Verification using Ada, Cambridge University Press, 1982
Sperschneider, V. & Antoniou,G: Logic: A Foundation for Computer Science, Addison-Wesley, to appear
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Antoniou, G., Sperschneider, V. (1990). On the verification of modules. In: Börger, E., Büning, H.K., Richter, M.M. (eds) CSL '89. CSL 1989. Lecture Notes in Computer Science, vol 440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52753-2_30
Download citation
DOI: https://doi.org/10.1007/3-540-52753-2_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52753-4
Online ISBN: 978-3-540-47137-0
eBook Packages: Springer Book Archive