The deductive synthesis of database transactions

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

The deductive synthesis of database transactions

Full text

Pdf (3.27 MB)

Source

ACM Transactions on Database Systems (TODS) archive
Volume 18 , Issue 4 (December 1993) table of contents

Pages: 626 - 677

Year of Publication: 1993

ISSN:0362-5915

Author

Xiaolei Qian

Stanford University

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 28, Citation Count: 1

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/169725.169716 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	BURSTALL, R. Formal description of program structure and semantics in first-order logic. Mach. Intel. 5 (1969), 79-98.
	2	Marco R. Casanova , Phillip A. Bernstein, A Formal System for Reasoning about Programs Accessing a Relational Database, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.386-414, July 1980 [doi>10.1145/357103.357111]
	3	E. F. Codd, A relational model of data for large shared data banks, Communications of the ACM, v.13 n.6, p.377-387, June 1970 [doi>10.1145/362384.362685]
	4	R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
	5	Ronald Fagin, Horn clauses and database dependencies, Journal of the ACM (JACM), v.29 n.4, p.952-985, Oct. 1982 [doi>10.1145/322344.322347]
	6	J. J. Finger, Exploiting constraints in design synthesis, Stanford University, Stanford, CA, 1987
	7	Johann Christoph Freytag , Nathan Goodman, On the translation of relational queries into iterative programs, ACM Transactions on Database Systems (TODS), v.14 n.1, p.1-27, March 1989 [doi>10.1145/62032.62033]
	8	GARDARIN, G., AND MELKANOFF, M. Proving consistency of database transactions. In Proceedings of the Fifth International Conference on Very Large Data Bases (1979)~ 291 298.
	9	GEORGEFF, M., AND LANSKY, A., Eds. Reasonzng about Actwns and Plans: Proceedzngs of the 1986 V~5~rkshop Morgan Kaufmann, Palo Alto, Calif., 1987.
	10	GIRARI), J-Y A new constructive logic Classmal lognc. Logzc Coraput (Aprfi 1991)
	11	GREEN, C. Apphcatlon of theorem proving to problem solving. In Proceedings of the Internatzonal Joznt Con/~rence on Artzfzczal Intelllge~zce (1969), 219 239
	12	HENSCHEN, L., MECuNE, W, AND NAQVI, S Compiling constraint-checking programs from first-order formulas. In Advances zn Database Theory, Vol 2, H Gallaire, J. Minker, and J-M. Nmolas, Eds., Plenum Press, New York, 1984, 145-170.
	13	Arding Hsu , Tomasz Imielinski, Integrity checking for multiple updates, Proceedings of the 1985 ACM SIGMOD international conference on Management of data, p.152-168, May 1985, Austin, Texas, United States
	14	KANT, E. On the efficient synthesis of efficient programs. Arttf Intell. 20, (1983), 253-305.
	15	Jonathan Jay King, Query optimization by semantic reasoning, 1981
	16	KOEN~G, S., AND PAICE, R A transformational framework for the automatic control of derived data. In Proceedlngs of the Seventh InternatLonal Conferelzce on Very Large Data Bases (1981), 306-318
	17	Zohar Manna , Richard Waldinger, A Deductive Approach to Program Synthesis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.90-121, Jan. 1980 [doi>10.1145/357084.357090]
	18	MANNA, Z., AND WALDINGER, R. Problematic features of programming languages: A mtua-
	19	Zohar Manna , Richard Waldinger, Special relations in automated deduction, Journal of the ACM (JACM), v.33 n.1, p.1-59, Jan. 1986 [doi>10.1145/4904.4905]
	20	MANNA, Z , AND WALI)INGER, R The deductive synthes~s of ~mperative LISP programs. In Proceedzngs of AAAI 11987), 155-160.
	21	Z. Manna , R. Waldinger, How to clear a block: A theory of plans, Journal of Automated Reasoning, v.3 n.4, p.343-377, Dec. 1987
	22	Zohar Manna , Richard Waldinger, The logical basis for computer programming: vol. 2, deductive systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	23	MARTELLI, A, AND ROSSI, G. An algorithm for umfication m equational theories. In Proceedtngs of the Third ~~mposlum on Loglc Programmzng (1986), 180-186.
	24	MARTIN-LoF, P An lntmtiomstlc theory of types: Predicative part. In Proceed~ng.~ of Logzc Colloquium 1973 (1975), 73 118.
	25	McCARTHY, J. Situations, actions, and causal laws. In Semantzc Information Processzng, M. Mmsky Ed, MIT Press, Cambridge, Mass, 1968, 410-417
	26	Chetan R. Murthy, Classical Proofs as Programs: How, What and Why, Cornell University, Ithaca, NY, 1991
	27	NICOLAS, J-M., AND GALLAIRE, H. Data base: Theory vs interpretation In Logzc and Databases, H. Gallmre and J. Minker, Eds., Plenum Press, New York, 1978, 33 54
	28	NICOLAS, J-M. Logic for improving integrity checking in relational data bases Acta Inf 18, (1982), 227 253
	29	PAIGE, R Applications of finite differencing to database integrity control and query/transaction optimization, in Advances l~7 Database Theoo', Vol 2, H Gallaire, J. Minker, and J-M. Nicolas, Eds., Plenum Press, New York, 1984, 171-209
	30	E. P. D. Pednault, Toward a mathematical theory of plan synthesis, Stanford University, Stanford, CA, 1987
	31	Xiaolei Qian , Gio Wiederhold, The deductive synthesis of database transactions, 1989
	32	X. Qian, An axiom system for database transactions, Information Processing Letters, v.36 n.4, p.183-189, Nov. 1990 [doi>10.1016/0020-0190(90)90070-E]
	33	Xiaolei Qian, The expressive power of the bounded-iteration construct, Acta Informatica, v.28 n.7, p.631-656, Oct. 1991 [doi>10.1007/BF01178680]
	34	Charles Rich , Richard C. Waters, Readings in artificial intelligence and software engineering, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1986
	35	Tim Sheard , David Stemple, Automatic verification of database transaction safety, ACM Transactions on Database Systems (TODS), v.14 n.3, p.322-368, Sept. 1989 [doi>10.1145/68012.68014]
	36	Douglas R. Smith, Top-down synthesis of divide-and-conquer algorithms, Artificial Intelligence, v.27 n.1, p.43-96, Sept. 1985 [doi>10.1016/0004-3702(85)90083-9]
	37	M E Stickel, Automated deduction by theory resolution, Journal of Automated Reasoning, v.1 n.4, p.333-355, 1985
	38	Jeffrey D. Ullman, Principles of database and knowledge-base systems, Vol. I, Computer Science Press, Inc., New York, NY, 1988
	39	WALD{NGER, R., AND LEE, R. PROW: A step toward automatic program writing. In Proceedings of the International Joint Conference on Artificial Intelligence (1969), 241 252.
	40	Gio C. Wiederhold, Database Design, McGraw-Hill, Inc., New York, NY, 1983