We present a theorem-prover based analysis tool for object-oriented database systems with integrity constraints. Object-oriented database specifications are mapped to higher-order logic (HOL). This allows us to reason about the semantics of database operations using a mechanical theorem prover such as Isabelle or PVS. The tool can be used to verify various semantics requirements of the schema (such as transaction safety, compensation, and commutativity) to support the advanced transaction models used in workflow and cooperative work. We give an example of method safety analysis for the generic structure editing operations of a cooperative authoring system.
CITATION STYLE
Spelt, D., & Even, S. (1999). A theorem prover-based analysis tool for object-oriented databases. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1579, pp. 375–389). Springer Verlag. https://doi.org/10.1007/3-540-49059-0_26
Mendeley helps you to discover research relevant for your work.