Translation of Z specifications to executable code: Application to the database domain |
| |
| Affiliation: | 1. School of Engineering and Science, Sharif University of Technology-International Campus, Kish Island, Iran;2. Department of Computer Engineering, Sharif University of Technology, Tehran, Iran;1. School of Engineering and Computer Science, The Hebrew University of Jerusalem, Edmond Safra Campus, 91904 Jerusalem, Israel;2. Department of Computer Engineering, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria;3. Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, 32 Vassar Street, 02139 Cambridge, MA, USA;1. College of Management, Yuan Ze University, 135 Yuan-Dung Road, Chung-Li, Taoyuan 320, Taiwan;2. Department of Information Management, National Chi Nan University, 470, University Road, Puli Nantou 545, Taiwan;1. Rochester Institute of Technology, Computer Science Department, New York, United States;2. Faculty of Electrical Engineering, Czech Technical University, Prague, Czech Republic;3. DCC-Faculty of Sciences & LIACC, University of Porto, Portugal;4. DI-University of Beira Interior & LIACC, University of Porto, Portugal;5. DCC-Faculty of Sciences & INESC TEC, University of Porto, Portugal |
| |
| Abstract: | ContextIt is well-known that the use of formal methods in the software development process results in high-quality software products. Having specified the software requirements in a formal notation, the question is how they can be transformed into an implementation. There is typically a mismatch between the specification and the implementation, known as the specification-implementation gap.ObjectiveThis paper introduces a set of translation functions to fill the specification-implementation gap in the domain of database applications. We only present the formal definition, not the implementation, of the translation functions.MethodWe chose Z, SQL and Delphi languages to illustrate our methodology. Because the mathematical foundation of Z has many properties in common with SQL, the translation functions from Z to SQL are derived easily. For the translation of Z to Delphi, we extend Delphi libraries to support Z mathematical structures such as sets and tuples. Then, based on these libraries, we derive the translation functions from Z to Delphi. Therefore, we establish a formal relationship between Z specifications and Delphi/SQL code. To prove the soundness of the translation from a Z abstract schema to the Delphi/SQL code, we define a Z design-level schema. We investigate the consistency of the Z abstract schema with the Z design-level schema by using Z refinement rules. Then, by the use of the laws of Morgan refinement calculus, we prove that the Delphi/SQL code refines the Z design-level schema.ResultsThe proposed approach can be used to build the correct prototype of a database application from its specification. This prototype can be evolved, or may be used to validate the software requirements specification against user requirements.ConclusionTherefore, the work presented in this paper reduces the overall cost of the development of database applications because early validation reveals requirement errors sooner in the software development cycle. |
| |
| Keywords: | Prototyping Database Formal methods Software development Graphical user interface |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
