Data Models and Data Manipulation Languages: Complementary Semantics and Proof Theory.

Alexander Borgida, Harry K. T. Wong: Data Models and Data Manipulation Languages: Complementary Semantics and Proof Theory. VLDB 1981: 260-271
  author    = {Alexander Borgida and
               Harry K. T. Wong},
  title     = {Data Models and Data Manipulation Languages: Complementary Semantics
               and Proof Theory},
  booktitle = {Very Large Data Bases, 7th International Conference, September
               9-11, 1981, Cannes, France, Proceedings},
  publisher = {IEEE Computer Society},
  year      = {1981},
  pages     = {260-271},
  ee        = {db/conf/vldb/BorgidaW81.html},
  crossref  = {DBLP:conf/vldb/81},
  bibsource = {DBLP,}


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.

Copyright © 1981 by The Institute of Electrical and Electronic Engineers, Inc. (IEEE). Abstract used with permission.

ACM SIGMOD Anthology

CDROM Version: Load the CDROM "Volume 1 Issue 4, VLDB '75-'88" and ... DVD Version: Load ACM SIGMOD Anthology DVD 1" and ... BibTeX

Printed Edition

Very Large Data Bases, 7th International Conference, September 9-11, 1981, Cannes, France, Proceedings. IEEE Computer Society 1981
Contents BibTeX


Marco A. Casanova, Philip A. Bernstein: A Formal System for Reasoning about Programs Accessing a Relational Database. ACM Trans. Program. Lang. Syst. 2(3): 386-414(1980) BibTeX
E. F. Codd: A Relational Model of Data for Large Shared Data Banks. Commun. ACM 13(6): 377-387(1970) BibTeX
E. F. Codd: Extending the Database Relational Model to Capture More Meaning. ACM Trans. Database Syst. 4(4): 397-434(1979) BibTeX
Stephen A. Cook: Soundness and Completeness of an Axiom System for Program Verification. SIAM J. Comput. 7(1): 70-90(1978) BibTeX
Edsger W. Dijkstra: A Discipline of Programming. Prentice-Hall 1976
Georges Gardarin, Michel A. Melkanoff: Proving Consistency of Database Transactions. VLDB 1979: 291-298 BibTeX
Irene Greif, Albert R. Meyer: Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer. ACM Trans. Program. Lang. Syst. 3(4): 484-507(1981) BibTeX
Michael Hammer, Dennis McLeod: Semantic Integrity in a Relational Data Base System. VLDB 1975: 25-47 BibTeX
C. A. R. Hoare: An Axiomatic Basis for Computer Programming. Commun. ACM 12(10): 576-580(1969) BibTeX
C. A. R. Hoare, Peter E. Lauer: Consistent and Complementary Formal Theories of the Semantics of Programming Languages. Acta Inf. 3: 135-153(1974) BibTeX
C. A. R. Hoare, Niklaus Wirth: An Axiomatic Definition of the Programming Language PASCAL. Acta Inf. 2: 335-355(1973) BibTeX
Ralph L. London, John V. Guttag, James J. Horning, Butler W. Lampson, James G. Mitchell, Gerald J. Popek: Proof Rules for the Programming Language Euclid. Acta Inf. 10: 1-26(1978) BibTeX
John Mylopoulos, Philip A. Bernstein, Harry K. T. Wong: A Language Facility for Designing Database-Intensive Applications. ACM Trans. Database Syst. 5(2): 185-207(1980) BibTeX
John Mylopoulos, Harry K. T. Wong: Some Features of the TAXIS Data Model. VLDB 1980: 399-410 BibTeX
Vaughan R. Pratt: Semantical Considerations on Floyd-Hoare Logic. FOCS 1976: 109-121 BibTeX
John Miles Smith, Diane C. P. Smith: Database Abstractions: Aggregation and Generalization. ACM Trans. Database Syst. 2(2): 105-133(1977) BibTeX

Referenced by

  1. Hervé Gallaire, Jack Minker, Jean-Marie Nicolas: Logic and Databases: A Deductive Approach. ACM Comput. Surv. 16(2): 153-185(1984)
  2. Ulrich Schiel: An Abstract Introduction to the Temporal-Hierarchic Data Model (THM). VLDB 1983: 322-330
ACM SIGMOD Anthology - DBLP: [Home | Search: Author, Title | Conferences | Journals]
VLDB Proceedings (1977-1981): Copyright © by IEEE,
ACM SIGMOD Anthology: Copyright © by ACM (, Corrections:
DBLP: Copyright © by Michael Ley (, last change: Sat May 16 23:45:12 2009