On the Validation of Invariants at Runtime

Article type: Research Article

Authors: Kosiuczenko, Piotr

Affiliations: Institute of Information Systems, WAT, Warszawa, Poland. pkosiuczenko@wat.edu.pl

Note: [] Address for correspondence: ISI, WAT, Kaliskiego 2, 00-908 Warszawa, Poland

Abstract: The paradigm of contractual specification provides a transparent way of specifying object-oriented systems. In this paradigm, system consistency is specified using so-called invariants. Runtime validation of invariants is a complex problem. Existing validation methods require either exhausting validation of an invariant for all objects of the corresponding class or the use of restrictive type systems. In this paper a non-exhaustive method of invariant validation is proposed. It is proved that the method is sound and an implementation of this method is discussed. It is shown also how to extract context free languages corresponding to OCL-invariants.

Keywords: OCL, contracts, invariant validation, framing, optimization

DOI: 10.3233/FI-2013-859

Journal: Fundamenta Informaticae, vol. 125, no. 2, pp. 183-222, 2013