SEMANTICS OF NETWORK DATA MANIPULATION LANGUAGES
Dipayan Gangopadhyay, Umeshwar Dayal, James C. Browne · 1982
and correctness of dml programs can be proved. An axiomatic basis for defining the semantics of navigational data manipulation languages is presented. This basis consists of an abstraction of the network data model achieved by three abstract data types, an assertion language to express Properties of database states, and a DML to Program the transactions. The proof rules of the DML constructs and the axioms defined on the data types can be used to establish the correctness of transactions. Potential applications of the proposed formalism in language design, semantic definition of existing languages, and integrity management, are outlined via examples. We start by treating the database as a collection of network structured objects, characterized by a few abstract data types (GUTT 781. We then define an assertion language for expressing properties of a database state in terms of functions and predicates defined on these abstract data types. We also propose a simple dml in which the transactions may be programmed. The dml statements are treated as assignments of network structured values to database objects. Therefore, their semantics can be given in the axiomatic style of Hoare (HOAR 741. Using the axioms of the dml statements and those of the abstract data types, we can prove that a dml program is correct: if the program is initiated in a database state characterized by a given assertion, we can show that upon completion of the program, the final database state satisfies another given assertion.