By the same authors

A behavioural notion of subtyping for object-oriented programming in SPARK95.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Author(s)

Department/unit(s)

Publication details

Title of host publicationRELIABLE SOFTWARE TECHNOLOGIES - ADA-EUROPE 2003
DatePublished - 2003
Pages309-321
Number of pages13
PublisherSPRINGER-VERLAG BERLIN
Place of PublicationBERLIN
EditorsJP Rosen, A Strohmeier
Original languageEnglish
ISBN (Print)3-540-40376-0

Abstract

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.

    Research areas

  • behavioural subtyping, modular reasoning, supertype abstraction, object-oriented programming, SPARK, SPECIFICATION, VERIFICATION

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations