Verification of object oriented programs using class invariants

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

A proof system is presented for the verification and derivation of object oriented programs with as main features strong typing, dynamic binding, and inheritance. The proof system is inspired on Meyer’s system of class invariants and remedies its unsoundness, which is already recognized by Meyer. Dynamic binding is treated in a flexible way: when throughout the class hierarchy overriding methods respect the pre- and postconditions of the overridden methods, very simple proof rules for method calls suffice; more powerful proof rules are supplied for cases where one cannot or does not want to follow this restriction. The proof system is complete relative to proofs for properties of pointers and the data domain.
Original languageEnglish
Title of host publicationFundamental Approaches to Software Engineering (Proceedings Third International Conference, FASE2000; held as part of ETAPS2000, Berlin, Germany, March 25-April 2, 2000)
EditorsT.S.E. Maibaum
Place of PublicationBerlin
PublisherSpringer
Pages208-221
ISBN (Print)3-540-67261-3
DOIs
Publication statusPublished - 2000

Publication series

NameLecture Notes in Computer Science
Volume1783
ISSN (Print)0302-9743

Cite this

Huizing, C., & Kuiper, R. (2000). Verification of object oriented programs using class invariants. In T. S. E. Maibaum (Ed.), Fundamental Approaches to Software Engineering (Proceedings Third International Conference, FASE2000; held as part of ETAPS2000, Berlin, Germany, March 25-April 2, 2000) (pp. 208-221). (Lecture Notes in Computer Science; Vol. 1783). Springer. https://doi.org/10.1007/3-540-46428-X_15