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
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- Lin, Tse-Min; McDermid, John A.: A behavioural notion of subtyping for object-oriented programming in SPARK95 (2003)
- Parkinson, Paul; Gasperoni, Franco: High-integrity systems development for integrated modular avionics using VxWorks and GNAT (2002)