Generation of database schemas from Z specifications

Automatic translation of a high-level specification language to an executable implementation would be highly useful in maximizing the benefits of formal methods. We will introduce a set of translation functions to fill the specification-implementation gap in the domain of database applications. Because the mathematical foundation of Z has many properties in common with SQL, a direct mapping from Z to SQL structures can be found. We derive a set of translation functions from Z to SQL for the generation of a database. The proposed methodology results in reducing the expenses and duration of the software development, and also, prevents the errors originated from the manual translation of specifications to code.