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

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element