A Behavioural Notion of Subtyping for Object-Oriented Programming in SPARK95

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 SPARK95, 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.