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