Abstract
In the context of the object-oriented data model, a compiletime approach is given that provides for a significant reduction of the amount of run-time transaction overhead due to integrity constraint checking. The higher-order logic Isabelle theorem prover is used to automatically prove which constraints might, or might not be violated by a given transaction in a manner analogous to the one used by Sheard and Stemple (1989) for the relational data model. A prototype transaction verification tool has been implemented, which automates the semantic mappings and generates proof goals for Isabelle. Test results are discussed to illustrate the effectiveness of our approach.
Original language | English |
---|---|
Title of host publication | Database Programming Languages |
Subtitle of host publication | 6th International Workshop, DBPL-6 Estes Park, Colorado, USA, August 18–20, 1997, Proceedings |
Editors | Sophie Cluet, Rick Hull |
Place of Publication | Berlin, Heidelberg |
Publisher | Springer |
Pages | 396-412 |
Number of pages | 17 |
ISBN (Electronic) | 1611-3349 |
ISBN (Print) | 0302-9743 |
DOIs | |
Publication status | Published - 1998 |
Event | 6th International Workshop on Database Programming Languages, DBPL 1997 - Estes Park, United States Duration: 18 Aug 1997 → 20 Aug 1997 Conference number: 6 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 1369 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Workshop
Workshop | 6th International Workshop on Database Programming Languages, DBPL 1997 |
---|---|
Abbreviated title | DBPL |
Country/Territory | United States |
City | Estes Park |
Period | 18/08/97 → 20/08/97 |
Keywords
- DB-PRJTM: TWENTE-MILANO
- DB-OODB: OBJECT-ORIENTED DATABASES
- Transaction verification
- Transaction semantics
- Object-oriented databases