Evaluation of Prototyping System for Formal Specification
| Project/Area Number |
07680373
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
FUKAZAWA Yoshiaki Waseda Univ, School of Sci.& Eng.Department of Information & Computer Science, Professor, 理工学部, 教授 (20165252)
|
|---|
| Project Period (FY) |
1995 – 1996
|
| Project Status |
Completed (Fiscal Year 1996)
|
| Budget Amount *help |
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 1996: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 1995: ¥1,400,000 (Direct Cost: ¥1,400,000)
|
|---|
| Keywords | Prototyping / Prototype / Formal Specification / Z / ZF notation / Set Theory / 述語論理 / 導出規則 / プログラム合成 |
|---|
| Research Abstract |
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
|
Report
(3 results)
Research Products
(12 results)
