Rule-based translation of specifications to executable code

It is well known that the use of formal methods in the software development process results in a high-quality software product. However, since formal approaches are just reasoning mechanisms, they do not offer defined ordered steps and guidance for moving between them. Refinement is a technique for moving between specifications but it bears very little resemblance to the real process of software design. An automatic translator from a specification language to an executable code would be highly useful in maximizing the benefits of formal methods. In the domain of database applications, we propose a rule-based algorithm to translate software requirements written in Z specifications to Delphi/SQL code. The approach transforms Z specifications to executable code via a set of formal rules and Delphi/SQL libraries. The libraries can be predefined or user-defined. The soundness of the translation process is examined by data refinement.