@inbook{cd91add25b97439083008f8ed423611a,
title = "Consistency of java transactions",
abstract = "A model of Java transactions is presented and the basic formal properties of this model with respect to behavioral compatibility and database integrity are proved. An implementation technique for incorporating constraints into the existing Java technology is developed, and a sophisticated theorem prover technology is integrated into this environment capable of enforcing behavioral compatibility and verifying transaction safety. The model of Java transactions developed in this paper is based on the subtle interplay of constraints, bounded parametric polymorphism and orthogonal persistence. The approach is based on a correct solution for extending Java with parametric polymorphism along with a technique for integrating logic-based constraints into Java class files and class objects. The Java Core Reflection is extended accordingly. The technique for enforcing database integrity constraints is based on the PVS theorem prover technology, and it combines static and dynamic checking to attain reasonable performance. The theorem prover technology is itself based on a sophisticated type system equipped with a form of semantic subtyping and parametric polymorphism. The higher-order features of this technology are proved to be critical in dealing with the problems of behavioral compatibility and transaction verification.",
author = "Suad Alagi{\'c} and Jeremy Logan",
year = "2004",
doi = "10.1007/978-3-540-24607-7_6",
language = "English",
isbn = "3540208968",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "71--89",
editor = "Georg Lausen and Dan Suciu",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}