Theorem Prover-Based Analysis Tool for Object-Oriented Databases

摘要

The authors present a theorem-prover based analysis tool for object-oriented211u001edatabase systems with integrity constraints. Object-oriented database 211u001especifications are mapped to higher-order logic (HOL). This allows us to reason 211u001eabout the semantics of database operations using a mechanical theorem power such 211u001eas Isabelle or PVS. The tool can be used to verify various semantics requirements 211u001eof the schema (such as transaction safety, compensation, and commutativity) to 211u001esupport the advanced transaction models used in workflow and cooperative work. 211u001eThe authors give an example of method safety analysis for the generic structure 211u001eediting operations of a cooperative authoring system.