A Proof Method for Correctness of Database Query Program


Article Preview

It is necessary that formal proof for correctness of relational algebra expressions. It can effectively improve the reliability of database query program. The aim of the present study is to present a proof method for correctness of relational algebra expressions. The basic idea about this proof method is explained as follows. Based on the semantics of relational algebra operators, according to the characteristic of relational algebra expressions, we can formally derivate the semantic of an algebra relational expression. And then we can compare this semantic with the specification. If they are equal logically, the relational algebra expression is correct, otherwise, the relational algebra expression is wrong. This article explains the mean and necessity of proving the correctness of relational algebra expressions. Some rules of formal deduction are presented. Based on it, we present a proof method for correctness of relational algebra expressions. Next, a application is given to illustrate this proof method. At last, conclusions and discussions about this proof method are given. As far as we known, there is no other work which is about proof method for the correctness of a relational algebra expression to the database query specification based on the given semantics.



Advanced Materials Research (Volumes 121-122)

Edited by:

Donald C. Wunsch II, Honghua Tan, Dehuai Zeng, Qi Luo




B. Yang "A Proof Method for Correctness of Database Query Program", Advanced Materials Research, Vols. 121-122, pp. 464-469, 2010

Online since:

June 2010





[1] E. Westbrook, A. Stump, and I. Wehrman, A language-based approach to functionally correct imperative programming, , Proc. of the 10th International Conference on Functional Programming (ICFP05), (2005).

DOI: https://doi.org/10.1145/1086365.1086400

[2] Douglas R. Smith. Comprehension by derivation, Proceedings of the 13th International Workshop on Program Comprehension, IEEE Computer Society Press, Los Alamitos, CA, May 2005, pp.3-9.

[3] Codd E. F, Relational completeness of data base sublanguages, Data Base Systems, Prentice Hall, (1972).

[4] David von Oheimb, and Thomas F. Gritaner, RALL: machine-supported proofs for relation algebra, Proceedings of CADE-14, Lecture Notes in Computer Science 1249(1997), 380-394.

DOI: https://doi.org/10.1007/3-540-63104-6_36

[5] Gu Tianlong, Formal methods of software development, Beijing: Higher education press, 2005. 1: 143-150.

[6] Jeremy E. Dawson, and Rajeev Gore, A mechanised proof system for relation algebra using display logic, http: /users. rsise. anu. edu. au/~rpg/Publications/MechanisedRA/dRA. ps. gz.

[7] Rudolf Berghammer, and Claudia Hattensperger, Computer-aided manipulation of relational expressions and formulae using RALF, Tech. Rep., Institut fur Informatik und Praktische Mathematik, Christian-Albrechts Universitat Zu Kiel, Kiel, Germany.

DOI: https://doi.org/10.1515/piko.2007.245

[8] Abraham Silberschatz, Database system concepts(Fourth Edition), Beijing: Higher Education Press, 2004. 4.

[9] Bin cao, Optimization of complex nested queries in relational databases, " Washington, DC, USA: IEEE Computer Society, Proceedings of the 22nd International Conference on Data Engineering Workshops (ICDEW, 06), Volume 00, 2006. 4.

DOI: https://doi.org/10.1109/icdew.2006.106

[10] John A. Dossey, Albert D. Otto, and Lawrence E. Spence, Discrete mathematics, mechanical industry press, (2007).

[11] Shin cheng Mu, Algebra of programming in Ada: dependent types for relational program derivation, Journal of Functional Programming, 19: 545-579 Cambridge University Press, (2009).

DOI: https://doi.org/10.1017/s0956796809007345

Fetching data from Crossref.
This may take some time to load.