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

@inproceedings{DBLP:conf/vldb/BorgidaW81,
  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, http://dblp.uni-trier.de}
}

Abstract

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.

ACM SIGMOD Anthology

CDROM Version: Load the CDROM "Volume 1 Issue 4, VLDB '75-'88" and ...

Windows: Click the letter of your CD drive
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
Mac: Click here
UNIX/LINUX: mount the CD and click on the path of your mount point:
/Anthology/vldb7588 or /cdrom

DVD Version: Load ACM SIGMOD Anthology DVD 1" and ...

Windows: Click the letter of your CD drive
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
Mac: Click here
UNIX/LINUX: mount the DVD and click on the path of your mount point:
/Anthology/aDVD1 or /dvd

Printed Edition

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

References

[1]: ...
[2]: 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)
[3]: E. F. Codd: A Relational Model of Data for Large Shared Data Banks. Commun. ACM 13(6): 377-387(1970)
[4]: E. F. Codd: Extending the Database Relational Model to Capture More Meaning. ACM Trans. Database Syst. 4(4): 397-434(1979)
[5]: Stephen A. Cook: Soundness and Completeness of an Axiom System for Program Verification. SIAM J. Comput. 7(1): 70-90(1978)
[6]: Edsger W. Dijkstra: A Discipline of Programming. Prentice-Hall 1976
[7]: Georges Gardarin, Michel A. Melkanoff: Proving Consistency of Database Transactions. VLDB 1979: 291-298
[8]: 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)
[9]: Michael Hammer, Dennis McLeod: Semantic Integrity in a Relational Data Base System. VLDB 1975: 25-47
[10]: C. A. R. Hoare: An Axiomatic Basis for Computer Programming. Commun. ACM 12(10): 576-580(1969)
[11]: C. A. R. Hoare, Peter E. Lauer: Consistent and Complementary Formal Theories of the Semantics of Programming Languages. Acta Inf. 3: 135-153(1974)
[12]: C. A. R. Hoare, Niklaus Wirth: An Axiomatic Definition of the Programming Language PASCAL. Acta Inf. 2: 335-355(1973)
[13]: ...
[14]: 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)
[15]: 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)
[16]: John Mylopoulos, Harry K. T. Wong: Some Features of the TAXIS Data Model. VLDB 1980: 399-410
[17]: ...
[18]: Vaughan R. Pratt: Semantical Considerations on Floyd-Hoare Logic. FOCS 1976: 109-121
[19]: John Miles Smith, Diane C. P. Smith: Database Abstractions: Aggregation and Generalization. ACM Trans. Database Syst. 2(2): 105-133(1977)
[20]: ...
[21]: ...
[22]: ...
[23]: ...