Axiomatic definitions for data model semantics

摘要

The axiomatic method, a widely accepted technique for the precise (formal) definition of programming language semantics, is used to define data model semantics. First, a definition of the term “data model” is developed. The strong relationship between database and programming language concepts is discussed. The nature of data model formalization is described. Based on the experience in programming languages, it is argued that the formal definition of a data model aids database design, database management system implementation, semantic integrity verification and validation, and data model theory. It is further argued that precision must be weighed against understandability, and that a degree of informality can be introduced without loss of precision. Several different formal description techniques and their particular advantages are mentioned. It is argued that in order to achieve desired goals, more than one technique be used to develop consistent and complementary formal definitions of a data model. The axiomatic method is described. Axiomatic definitions are particularly appropriate for the design, analysis, and comparison of schemas, transactions, and databases. The axiomatic definition technique is demonstrated in an annotated, precise definition of the semantics of the structural aspects of a semantic data model which is based on the relational data model.