Reasonong about Classess in Object-Oriented Languages: Logical Models and Tools

Ulrich Hensel, Marieke Huisman, Bart Jacobs, Hendrik Tews

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

33 Citations (Scopus)

Abstract

A formal language CCSL is introduced for describing specifications of classes in object-oriented languages. We show how class specifications in CCSL can be translated into higher order logic. This allows us to reason about these specifications. In particular, it allows us (1) to describe (various) implementations of a particular class specification, (2) to develop the logical theory of a specific class specification, and (3) to establish refinements between two class specifications.

We use the (dependently typed) higher order logic of the proof-assistant PVS, so that we have extensive tool support for reasoning about class specifications. Moreover, we describe our own front-end tool to PVS, which generates from CCSL class specifications appropriate PVS theories and proofs of some elementary results.
Original languageEnglish
Title of host publicationProgramming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings
EditorsChris Hankin
PublisherSpringer
Pages105-121
Number of pages17
ISBN (Electronic)978-3-540-69722-0
ISBN (Print)978-3-540-64302-9
DOIs
Publication statusPublished - 1998
Externally publishedYes
Event7th European Symposium on Programming, ESOP 1998 - Lisbon, Portugal
Duration: 28 Mar 19984 Apr 1998
Conference number: 7

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume1381

Conference

Conference7th European Symposium on Programming, ESOP 1998
Abbreviated titleESOP 1998
Country/TerritoryPortugal
CityLisbon
Period28/03/984/04/98

Fingerprint

Dive into the research topics of 'Reasonong about Classess in Object-Oriented Languages: Logical Models and Tools'. Together they form a unique fingerprint.

Cite this