Donald Bren School of Information and Computer Sciences

This paper presents a method for the specification, verification, and enforcement of semantic integrity using behavioral abstraction. The specification contains both the abstract invariant of the abstract object (the static characteristics of the data) and the legal operations on the objects as defined by pre and post conditions (the behavioral characteristics) which preserve this invariant. The integrity specifications can be verified by proving that the abstract operations preserve this invariant. A practical means for enforcing integrity leads naturally from this integrity specification technique.