Data models and data manipulation languages: complementary semantics and proof theory
Alexander T. Borgida, Harry K. T. Wong · Very Large Data Bases · 1981
We present briefly a language which integrates the description of a data model, data manipulation language and integrity constraints into one coherent framework, resembling that proposed by several recent papers in the field of semantic data models. We then give two formal specifications of the semantics of the model and DML: one, based on states and state transitions, intended for database implementors and programmers, and one, based on axioms and partial correctness assertions intended for verifiers who wish to show that the system maintains integrity constraints. Most significantly, we sketch the proof that the deductive theory is sound and relative complete and hence matches the state transition semantics.