A Formal System for Reasoning about Programs Accessing a Relational Database

ABSTRACT

A formal system for proving properties of programs accessing a database is introduced. Proving that a program preserves consistency of the database is one of the possible applications of the system. The formal system is a variant of dynamic logic and incorporates a data definition language (DDL) for describing relational databases and a data manipulation language (DML) whose programs access data in a database. The DDL is a many-sorted first-order language that accounts for data aggregations. The DML features a many-sorted assignment in place of the usual data manipulation statements, in addition to the normal programming language constructs.

REFERENCES

• 1: Alfred V. Aho , Jeffrey D. Ullman, Universality of data retrieval languages, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.110-119, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567763]
• 2: BANCILHON, F. On the completeness of query languages for relational data bases. In Proc. 7th Symp. Math. Foundations of Computer Science, Zakopane, Poland (Lecture Notes in Computer Science, Springer-Verlag, New York, Sept. 1978).
• 3: BERNSTEIN, P.A., ET AL. A formal model of concurrency control mechanisms for database systems. IEEE Trans. Softw. Eng. (May 1979).
• 4: Philip A. Bernstein , David W. Shipman , James B. Rothnie, Jr., Concurrency control in a system for distributed databases (SDD-1), ACM Transactions on Database Systems (TODS), v.5 n.1, p.18-51, March 1980 [doi>10.1145/320128.320131]
• 5: CASANOVA, M.A. The concurrency control problem for database systems. Ph.D. dissertation, Harvard Univ., Cambridge, Mass., Nov. 1979.
• 6: Marco A. Casanova , Philip A. Bernstein, The logic of a relational data manipulation language, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.101-109, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567762]
• 7: CHAMBERLiN, D.D., ET AL. SEQUEL-2: A unified approach to data definition manipulation and control. Tech. Rep. RJ 1798, IBM, New York, June 1976.
• 8: Ashok K. Chandra , David Harel, Computable queries for relational data bases (Preliminary Report), Proceedings of the eleventh annual ACM symposium on Theory of computing, p.309-318, April 30-May 02, 1979, Atlanta, Georgia, United States [doi>10.1145/800135.804423]
• 9: Edmund Melson Clarke, Jr., Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems, Journal of the ACM (JACM), v.26 n.1, p.129-147, Jan. 1979 [doi>10.1145/322108.322121]
• 10: CODO, E.F. A database sublanguage founded on the relational calculus. In Proc. 1971 ACM- SiGFIDET Workshop on Data Description, Access and Control.
• 11: 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]
• 12: COOK, S.A. Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 1 (Feb. 1978).
• 13: DAYAL, U. Schema mapping problems in database systems. Ph.D. dissertation, Harvard Univ., Cambridge, Mass., Aug. 1979.
• 14: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 15: ENDERTON, H.B. A Mathematical Introduction to Logic. Academic Press, New York, 1972.
• 16: ESWARAN, K.P. Specifications, implementations and interactions of a trigger subsystem in an integrated database system. Tech. Rep. RJ1820, IBM, New York, Aug. 1976.
• 17: K. P. Eswaran , J. N. Gray , R. A. Lorie , I. L. Traiger, The notions of consistency and predicate locks in a database system, Communications of the ACM, v.19 n.11, p.624-633, Nov. 1976 [doi>10.1145/360363.360369]
• 18: FLON, L., AND SUZUKI, N. Nondeterminism and the correctness of parallel programs. Presented at the IFIP Conf. Working Group on Formal Specifications of Programming Languages, Aug. 1977.
• 19: GARDARIN, G., AND MELKANOFF, M. Proving consistency of database transactions. In Proc. 1979 Int. Conf. Very Large Data Bases, Oct. 1979, pp. 291-298.
• 20: David Harel, First-Order Dynamic Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 21: HELl), G. D., STONEBRAKER, M.R., AND WONC, E. INGRES--A relational database system. In Proc. 1975 AFIPS NCC, AFIPS Press, Arlington, Va., pp. 409-416.
• 22: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 23: Information management system virtual storage (IMS/VS) general information manual. IBM no. GH20-1260, IBM, New York.
• 24: LAMPORT, L. Towards a theory of correctness for multi-user data base system. Tech. Rep. TR- CA-7610-0712, Massachusetts Computer Associates, Oct. 1976.
• 25: Jack Minker, Search strategy and selection function for an inferential relational system, ACM Transactions on Database Systems (TODS), v.3 n.1, p.1-31, March 1978 [doi>10.1145/320241.320242]
• 26: J. M. Nicolas, First order logic formalization for functional, multivalued and mutual dependencies, Proceedings of the 1978 ACM SIGMOD international conference on management of data, May 31-June 02, 1978, Austin, Texas [doi>10.1145/509252.509269]
• 27: PAPADIMITRIOU, C.H., BERNSTEIN, P.A., AND ROTHNIE, J.B. Some computational problems related to database concurrency control. In Proc. Conf. Theoretical Computer Science, Aug. 1977, pp. 275-282.
• 28: PRATT, V.R. Semantical considerations on Floyd-Hoare logic. In Proc. 17th IEEE Symp. Foundations of Computer Science, Oct. 1976, pp. 109-120.
• 29: Joachim W. Schmidt, Some high level language constructs for data of type relation, ACM Transactions on Database Systems (TODS), v.2 n.3, p.247-261, Sept. 1977 [doi>10.1145/320557.320568]
• 30: SHOENFIELD, J.R. Mathematical Logic. Addison-Wesley, Reading, Mass., 1967.
• 31: STEARNS, R.E., ET AL. Concurrency control for database systems. In Proc. 17th IEEE Syrup. Foundations of Computer Science, Oct. 1976, pp. 19-32.
• 32: Michael Stonebraker, Implementation of integrity constraints and views by query modification, Proceedings of the 1975 ACM SIGMOD international conference on Management of data, May 14-16, 1975, San Jose, California [doi>10.1145/500080.500091]
• 33: Michael Stonebraker , Gerald Held , Eugene Wong , Peter Kreps, The design and implementation of INGRES, ACM Transactions on Database Systems (TODS), v.1 n.3, p.189-222, Sept. 1976 [doi>10.1145/320473.320476]
• 34: Robert H. Thomas, A Majority consensus approach to concurrency control for multiple copy databases, ACM Transactions on Database Systems (TODS), v.4 n.2, p.180-209, June 1979 [doi>10.1145/320071.320076]
• 35: VAN EMI)EN, M.H. Computation and deductive information retrieval. Presented at the IFIP Conf. Working Group on Formal Specifications of Programming Languages, Aug. 1977.

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.4 Systems
          Subjects: Relational databases

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Languages, Management, Performance, Theory