Development Of Relational Algebra To Relational Calculus Conversion System

In the field of program verification, Hoare axiomatic method and the Dijkstra weakest pre-verb is the most outstanding of these two methods is their point system, the definition of the language system, and then find their way to the semantics of the language system. Formal research software, we found this problem: how to explore the database program, the semantics of relational algebra statements, where the database program that is operated with relations written in programming languages including relational operations procedures.Both Hoare axiomatic method or Dijkstra weakest pre-predicate method, each defined language system did not touch the database in the field. PAR method of Apla one of the characteristics of language is to relational algebra operations into programming languages, which makes Apla database program can be directly used for the development. Today the reality is, the program will inevitably deal with the database, so this part of the process of verification needed expansion of theoretical breakthrough.After a long in-depth research, we find that the core authentication database program is to find the database relational algebra semantics, further, that is, to convert into an equivalent relational algebra relational calculus.This paper studies the relationship between relational algebra to the calculus of transformation rules, and simplified the traditional transformation rules to expand. For the relational algebra to the relational calculus of transformation rules, this change mainly to solve the dual operation, we found more computing re-defined with a very complex transformation rules, What can multiple operations from a single weight or double the computing multi-step to achieved. Background paper developed a conversion system algorithm module, and made into the form of DLL components. Then developed a DLL component and assembled into a complete system GUI conversion system.Conversion system can automatically generate a given relational algebra and relational calculus equivalent results, so that makes program verification in the field to expand to the database, providing a possibility.