| Co-Investigator(Kenkyū-buntansha) |
KAWAGUCHI Nobuo Dept.of Engineering, Nagoya Univ., Assistant Professor, 工学研究科, 助手 (10273286)
YUEN Shoji Dept.of Engineering, Nagoya Univ., Assistant Professor, 工学研究科, 助手 (70230612)
AGUSA Kiyoshi Dept.of Engineering, Nagoya Univ., Professor, 工学研究科, 教授 (90026360)
INAGAKI Yasuyoshi Dept.of Engineering, Nagoya Univ., Professor, 工学研究科, 教授 (10023079)
SAKABE Toshiki Dept.of Engineering, Nagoya Univ., Professor, 工学研究科, 教授 (60111829)
|
|---|
| Research Abstract |
Technologies verifying whether a program works according to the specification is important for improvement of software reliability. Since it is impossible to verify programs completely automatically, a system verifying software interactively is expected.
On developing such a verificat ion system, the following merits will come by keeping specification language, programming language, verification language and system describing language in the same language. Programrs, werifiers, and verification system developers have to learn only one kind of language. This is a significant advantage, because they must learn more than three kind of languages if the languages are different.
The language covering all processes of software specification, implementation, verification and development of verification system (called meta language), should provide properties desirable as each language. In particular, it needs to be provided with a clear logic that is a basis of verification and provided with a function to operate programs and specifications, i.e.meta computation, as a development language of verification system. It is also provides an easy implementation of interactive control of verification processes.
Through these two years, we have examined confluence of dynamic term rewriting systems, a class of term rewriting systems in which the functional strategy is normalizing, strategy for overlapping term rewriting systems, and a method for efficient concurrent-execution of term rewriting systems and got several results.
|
