A Behavioural Notion of Subtyping for Object-Oriented Programming in SPARK95
T.-M. Lin and J.A. McDermid
The dynamic aspects of the object-oriented paradigm have prevented the adoption of the latter for the implementation of high integrity systems using the SPARK approach. This paper presents a proposal that allows object-oriented programming in SPARK 95, whereas supporting SPARK's static approach for verification by imposing a notion of behavioural subtyping between a type and all its subtypes. Behavioural subtyping supports modular reasoning through supertype abstraction, hence all proofs can be discharged based only on nominal/declared types. An example of proof is also presented.
Download Not Available
BibTex Entry
@inproceedings{Lin2003,
author = {T.-M. Lin and J.A. McDermid},
booktitle = {Reliable Software Technologies---Ada-Europe 2003},
editor = {J.-P. Rosen and A. Strohmeier},
note = {behavioural subtyping, modular reasoning, supertype abstraction, object-oriented programming, SPARK},
pages = {309-321},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {A Behavioural Notion of Subtyping for Object-Oriented Programming in SPARK95},
volume = {2655},
year = {2003}
}