More Web Proxy on the site http://driver.im/

Article

Free access

A transaction logic for database specification

Authors:

Richard WaldingerAuthors Info & Claims

SIGMOD '88: Proceedings of the 1988 ACM SIGMOD international conference on Management of data

Pages 243 - 250

https://doi.org/10.1145/50202.50232

Published: 01 June 1988 Publication History

Abstract

We introduce a logical formalism for the specification of the dynamic behavior of databases. The evolution of databases is characterized by both the dynamic integrity constraints which describe the properties of state transitions and the transactions whose executions lead to state transitions. Our formalism is based on a variant of first-order situational logic in which the states of computations are explicit objects. Integrity constraints and transactions are uniformly specifiable as expressions in our language. We also point out the application of the formalism to the verification and synthesis of transactions.

References

[1]

Abadl, Martin, "Temporal-logic Theorem Proving", PhD Dlssertatmn, Tech Rep STAN-CS-87-1151, Dept Comp Scmnce, Stanford Unlv, Mar 1987

Digital Library

[2]

Ablteboul, S, Vlanu, V, "A Transaction Language Complete for Database Update and Speclficahon", Proc 6th ACM SIGACT-SIGMOD Syrup Principles of Database Systems, 1987, 260-268

Digital Library

[3]

Brodm, M, "On Modelling Behavloural Semantics of Data", Proc 7th Int'l Conf VLDB, 1981, 32-42

[4]

Burstall, R, "Formal Description of Program Structure and Semantics m F~rst-order Log,c", Machine Intelhgence 5, B Meltzer and D Mlchle (editor), Edinburgh Umverslty Press, Edinburgh, Scotland, 1969, 79-98

[5]

Casanova, M, Bernstem, P, "A Formal System for Reasoning about Programs Accessing a Relational Database", ACM Trans Programming Languages and Systems, Vol 2, No 3, July 1980, 386-414

Digital Library

[6]

Castdho, J, Casanova, M, Furtado, A, "A Temporal Framework for Database Specifications", Proc 8$h lnt'l Conf VLDB, 1982, 280-291

Digital Library

[7]

Chfford, J, Warren, D, "Formal Semantics for Time m Databases", ACM Trans on Database Systems, Vol 8, No 2, June 1983, 214-254

Digital Library

[8]

Ehnch, R, Llpeck, U, Gogolla, M, "Speclficatmn, Semantics, and Enforcement of Dynanuc Database Constraints", Proc lOth Int'l Conf VLDB, 1984, 301-308

Digital Library

[9]

Gardarm, G, Melkanoff, M, "Proving Consistency of Database Transactmns", Proc 5th Int'l Conf VLDB, 1979, 291-298

[10]

Green, C, "Application of Theorem Proving to Problem Solving", Proc IJCAI, Washington, D C, May 1969, 219-239

[11]

Kung, C, "On Verification of Database Temporal Constraints", Proc ACM SIGMOD Conf, 1985, 169-179

Digital Library

[12]

Manchanda, S, Warren, D, "Towards a Logical Theory of Database Updates", Tech Rep 86/19, Dept Computer Science, State Untvermty of New York at Stony Brook, jul 1986

[13]

Manna, Z, Waldmger, R, "A Deductive Apploach to Program Synthesis", ACM Trans Programming Languages and Systems, Vol 2, No 1, Jan 1980, 90- 121

Digital Library

[14]

Manna, Z, Waldmger, R, "Problematic Features of Programming Languages A Situational-logic Approach", Acta lnformat~ca, Vol 16, 1981, 371-426

[15]

Manna, Z, Waldmger, It, "How to Clear a Block A Theory of Plans", Journal of Automated Reasoning, Vol 3, No 4, Dec 1987, 343-377

Digital Library

[16]

Manna, Z, Waldlnger, R, "The Deductive Synthesis of Imperative Msp Programs", Proc AAAI, Seattle, Aug 1987, 155-160

[17]

Manna, Z, Waldmger, R, The Logical Basis for Computer Programming, Vol 2 Deductive Techtuques, Addmon-Wesley, to be pubhshed

Digital Library

[18]

McCarthy, J, "Sltuatmns, Actmns, and Causal Laws", Semantic Informatmn Processing, l~i l~iinsky (e&tor), MIT Press, Cambridge, Ma.sq, 1968, 410-417

[19]

Sheard, T, Stemple, D, "Automatic Verlficatmn of Database Transactmn Safety", Corns Tech Report 86-30, Unlv Massachusetts at Amherst, 1986

Digital Library

[20]

Vlanu, V, "Dynamic Constraints and Database Evolution", Proc 2nd ACM SIGACT-SIGMOD Symp Prmczples of Database Systems, 1983

Digital Library

[21]

Waldlnger, R, Lee, R, "PROW A Step Toward Automatlc Program Writing', Proc IJCAI, W~hington, D C, May 1969, 241-252

[22]

Wmderhold, G and EiMasn, R, "The Structural Model for Database Design', Entlty-Relatmnsh~p Approach to System Analysts and Design, P Chen (editor), North Holland, Amsterdam, 1980

Digital Library

Cited By

Deng YFrankl PChays DRoman GGriswold WNuseibeh B(2005)Testing database transactions with AGENDAProceedings of the 27th international conference on Software engineering10.1145/1062455.1062486(78-87)Online publication date: 15-May-2005
https://dl.acm.org/doi/10.1145/1062455.1062486
Yuetang Deng Frankl PChays D(2005)Testing database transactions with AGENDAProceedings. 27th International Conference on Software Engineering, 2005. ICSE 2005.10.1109/ICSE.2005.1553550(78-87)Online publication date: 2005
https://doi.org/10.1109/ICSE.2005.1553550
Bækgaard L(2005)Transaction-based specification of database evolutionConceptual Modeling — ER '9710.1007/3-540-63699-4_11(127-140)Online publication date: 29-Jul-2005
https://doi.org/10.1007/3-540-63699-4_11
Show More Cited By

Index Terms

A transaction logic for database specification
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
  2. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Information systems
  1. Data management systems
    1. Database design and models
    2. Database management system engines
      1. Database transaction processing

Recommendations

A transaction logic for database specification

We introduce a logical formalism for the specification of the dynamic behavior of databases. The evolution of databases is characterized by both the dynamic integrity constraints which describe the properties of state transitions and the transactions ...
Specification of transaction systems protocols
Denotational semantics using horn concurrent transaction logic
ICLP'05: Proceedings of the 21st international conference on Logic Programming

In this work we propose to use a Horn fragment of Concurrent Transaction Logic ( ${\mathcal CTR}$) as an intuitive logic framework to specify semantics of concurrent programming languages.

Using Horn logic to specify a programming language has been ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SIGMOD '88: Proceedings of the 1988 ACM SIGMOD international conference on Management of data

June 1988

443 pages

ISBN:0897912683

DOI:10.1145/50202

ACM SIGMOD Record Volume 17, Issue 3
June 1988
431 pages
ISSN:0163-5808
DOI:10.1145/971701
Issue’s Table of Contents

Copyright © 1988 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGMOD: ACM Special Interest Group on Management of Data

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 June 1988

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

SIGMOD88

Sponsor:

SIGMOD

SIGMOD88: International Conference On Management of Data

June 1 - 3, 1988

Illinois, Chicago, USA

Acceptance Rates

Overall Acceptance Rate 785 of 4,003 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
2,112
Total Downloads

Downloads (Last 12 months)1,526
Downloads (Last 6 weeks)720

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Deng YFrankl PChays DRoman GGriswold WNuseibeh B(2005)Testing database transactions with AGENDAProceedings of the 27th international conference on Software engineering10.1145/1062455.1062486(78-87)Online publication date: 15-May-2005
https://dl.acm.org/doi/10.1145/1062455.1062486
Yuetang Deng Frankl PChays D(2005)Testing database transactions with AGENDAProceedings. 27th International Conference on Software Engineering, 2005. ICSE 2005.10.1109/ICSE.2005.1553550(78-87)Online publication date: 2005
https://doi.org/10.1109/ICSE.2005.1553550
Bækgaard L(2005)Transaction-based specification of database evolutionConceptual Modeling — ER '9710.1007/3-540-63699-4_11(127-140)Online publication date: 29-Jul-2005
https://doi.org/10.1007/3-540-63699-4_11
Yoon IKim HBae DYoun C(2000)Reliable Transaction Design Using MTS24th International Computer Software and Applications Conference10.5555/645982.674782(357-362)Online publication date: 25-Oct-2000
https://dl.acm.org/doi/10.5555/645982.674782
I-Chul Yoon Hyung-Ho Kim Cheong Youn Doo-Hwan Bae (2000)Reliable transaction design using MTSProceedings 24th Annual International Computer Software and Applications Conference. COMPSAC200010.1109/CMPSAC.2000.884748(357-362)Online publication date: 2000
https://doi.org/10.1109/CMPSAC.2000.884748
Chomicki J(1995)Efficient checking of temporal integrity constraints using bounded history encodingACM Transactions on Database Systems10.1145/210197.21020020:2(149-186)Online publication date: 1-Jun-1995
https://dl.acm.org/doi/10.1145/210197.210200
Sun WYu C(1994)Semantic Query Optimization for Tree and Chain QueriesIEEE Transactions on Knowledge and Data Engineering10.1109/69.2730336:1(136-151)Online publication date: 1-Feb-1994
https://dl.acm.org/doi/10.1109/69.273033
Tari Z(1993)ERC++Proceedings of the second international conference on Information and knowledge management10.1145/170088.170443(625-634)Online publication date: 1-Dec-1993
https://dl.acm.org/doi/10.1145/170088.170443
Chomicki JNiwiński DBeeri C(1993)On the feasibility of checking temporal integrity constraintsProceedings of the twelfth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems10.1145/153850.153876(202-213)Online publication date: 1-Aug-1993
https://dl.acm.org/doi/10.1145/153850.153876
Chomicki J(1992)History-less checking of dynamic integrity constraints[1992] Eighth International Conference on Data Engineering10.1109/ICDE.1992.213153(557-564)Online publication date: 1992
https://doi.org/10.1109/ICDE.1992.213153
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents