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.
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 language | English |
---|---|
Title of host publication | Programming 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 |
Editors | Chris Hankin |
Publisher | Springer |
Pages | 105-121 |
Number of pages | 17 |
ISBN (Electronic) | 978-3-540-69722-0 |
ISBN (Print) | 978-3-540-64302-9 |
DOIs | |
Publication status | Published - 1998 |
Externally published | Yes |
Event | 7th European Symposium on Programming, ESOP 1998 - Lisbon, Portugal Duration: 28 Mar 1998 → 4 Apr 1998 Conference number: 7 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 1381 |
Conference
Conference | 7th European Symposium on Programming, ESOP 1998 |
---|---|
Abbreviated title | ESOP 1998 |
Country/Territory | Portugal |
City | Lisbon |
Period | 28/03/98 → 4/04/98 |