A theorem prover-based analysis tool for object-oriented databases

10Citations
Citations of this article
4Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free