Evaluation of Prototyping System for Formal Specification

在软件开发中，有必要准确地分析和定义所需的属性和功能。为此，形式规范扮演着重要的角色，许多形式规范语言已经被提出。在这些语言中，被广泛采用的是基于Zermelo-Frankel集合论的规范语言Z。在Z语言中，根据替换公理，方案中的每个部分函数都应该是单值的，如果完全定义了规格说明，从而可以证明所包含的部分函数是单值的，则关于其设计和实现的描述经常在规格说明中混杂地指定。为了使替换公理的描述完备，描述语言必须保证部分函数是隐含的单值函数。因此，我们定义了ZZ语言，其中的部分函数可以用不完全定义来描述。此外，我们还介绍了执行规范，它提供了有关其设计和实现的信息。将规范和执行规范分离，保持了对所需软件的高层次描述，实现了规范及其执行规范的原型化

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