Evaluation of Prototyping System for Formal Specification

点击翻译按钮获取中文摘要

In software development, it is necessary to analyze and define exactly what properties and functions are required. For this purpose, formal specification plays a significant role, and many formal specification languages have been proposed. In these languags, Specification language Z,which is based on Zermelo-Frankel set theory, is widely adopted. In language Z,every partial function in schemes, shall be single-valued according to the axiom of replacement, If specification is defined completely so that it can be proved that contained the partial functions are single-valued, descriptions concerning its design and its implementation are often mixedly specified in the specification. In order to make the specification omplete for the axiom of replacement, it is necessary that the description language assures partial functions are single-valued implicitly. Therefore, we defined language ZZ,in which a partial function can be described with the incomplete definitions. Furthermore, we introduced the execution specification which gives information about its design and implementation. The separation into the specification and the execution specification keeps the description for the required software high-level and realizes the prototyping of the specification with its execution specification