×

SPARK95

swMATH ID: 3386
Software Authors: Lin, Tse-Min; McDermid, John A.
Description: 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.
Homepage: http://i12www.ira.uka.de/~engelc/lehre/seminarSS07/material/SPARK95.pdf
Keywords: behavioural subtyping; modular reasoning; supertype abstraction; object-oriented programming; SPARK
Related Software:
Referenced in: 2 Publications

Referenced in 0 Serials

Referenced in 1 Field

2 Computer science (68-XX)

Referencing Publications by Year