Evaluation of Prototyping System for Formal Specification

形式规范原型系统的评估

• 批准号: 07680373
• 负责人: FUKAZAWA Yoshiaki
• 金额: $ 1.41万
• 依托单位: Waseda University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 1995
• 资助国家: 日本
• 起止时间: 1995 至 1996
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-07680373/
• 关键词: Prototyping; Prototype; Formal Specification; Z; ZF notation; Set Theory; 述語論理; 導出規則; プログラム合成

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

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

项目成果

J.Baeg and Y.Fukazawa: "A Backward Navigator and its User Model" Proc.of 2nd.Joint Conf.on Knawledge Bared Software Eng. Vol.2. 310-317 (1996)

J.Baeg 和 Y.Fukazawa：“向后导航器及其用户模型”Proc.of 2nd.Joint Conf.on Knawledge Bared Software Eng。

小野康一,深澤良彰: "実行時仕様記述言語ZXの導入による高レベル形式的仕様の実行" レクチャーノート/ソフトウェア学. 15. 121-130 (1996)

Koichi Ono、Yoshiaki Fukasawa：“通过引入运行时规范语言 ZX 执行高级形式规范”讲义/软件研究。15. 121-130 (1996)

J.Baeg and Y.Fukazawa: "A Backward Navigator and its User Model" Proc. 2nt Conf. on Knowledge Based Softwave Eng.Vol. 2. 310-317 (1996)

J.Baeg 和 Y.Fukazawa：“向后导航器及其用户模型”Proc。

荒崎秀一,深澤良彰: "ドメインモデルを利用したプログラム理解支援について" ソフトウェア開発のためのドメイン分析・モデリング技術シンポジウム. 123-132 (1996)

Shuichi Arasaki、Yoshiaki Fukasawa：“使用领域模型支持程序理解”软件开发领域分析和建模技术研讨会 123-132 (1996)。

荒崎秀一,深澤良彰: "ドメインモデルを利用したプログラム理解支援について" ソフトウェア開発のためのドメイン分析・モデリングシンポジウム. 123-132 (1996)

Shuichi Arasaki、Yoshiaki Fukasawa：“使用领域模型支持程序理解”软件开发领域分析和建模研讨会 123-132 (1996)。