| 講演名 | 1999/11/12 検証を考慮した仕様記述の指針に関する研究 五百蔵 重典, 緒方 和博, 二木 厚吉, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 代数仕様言語は,仕様が実行可能であるという特徴を利用して,仕様をプロトタイプと見倣せたり,検証の半自動化を実現できる.しかし,代数仕様言語が実用に供するには,モジュールを効率よく扱え書換え速度が高速な処理系が必要である.本研究では,実行効率のよい代数仕様言語CafeOBJの処理系を作成し,その処理系が正しく動くことを示すために,以下のことを行った.CafeOBJのモジュールシステムの要求と設計をCafeOBJを用いて記述し,設計が要求を満たしていることを振舞等価の概念を用いて示した.そしてこの仕様記述および検証で得られた仕様記述の際に得られた知見をまとめた. |
| 抄録(英) | Because algebraic specification languages are executable, we regard a specification written using there as prototype and verify a specification (semi-)automatically. For algebraic specification languages worth usage, we need highly efficient its processes. Although we need specification languages having processor dealing with many modules efficiently for its experiments and verifications, it is few research about processors of such specification language. We begun the design of highly efficient CafeOBJ processors. Then, we wanted to implement while keeping correct. In this paper, we formally specified the requirement and design of CafeOBJ module system with CafeOBJ. We showed functionality equality between requirement and design using behaviour equivalence. We summarize information which was known from the experiment describing and verifying the specification. |
| キーワード(和) | 指針 / 検証 / 仕様 / モジュール / CafeOBJ / Standard ML |
| キーワード(英) | guideline / verification / specification / module / CafeOBJ / Standard ML |
| 資料番号 | KBSE99-41 |
| 発行日 |
| 研究会情報 | |
| 研究会 | KBSE |
|---|---|
| 開催期間 | 1999/11/12(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Knowledge-Based Software Engineering (KBSE) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 検証を考慮した仕様記述の指針に関する研究 |
| サブタイトル（和） | |
| タイトル（英） | A Study of Guidelines of Describing Specification Considering Verification |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 指針 / guideline |
| キーワード(2)（和/英） | 検証 / verification |
| キーワード(3)（和/英） | 仕様 / specification |
| キーワード(4)（和/英） | モジュール / module |
| キーワード(5)（和/英） | CafeOBJ / CafeOBJ |
| キーワード(6)（和/英） | Standard ML / Standard ML |
| 第 1 著者 氏名（和/英） | 五百蔵 重典 / Shigenori Ioroi |
| 第 1 著者 所属（和/英） | 神奈川工科大学工学部情報工学科 Dept. of Information and Computer Sciences, Kanagawa Institute of Technology |
| 第 2 著者 氏名（和/英） | 緒方 和博 / Kazuhiro Ogata |
| 第 2 著者 所属（和/英） | 北陸先端科学技術大学院大学情報科学研究科 Graduate School of Information Science, Japan Advanced Institute of Science and Technology |
| 第 3 著者 氏名（和/英） | 二木 厚吉 / Kokichi Futatsugi |
| 第 3 著者 所属（和/英） | 北陸先端科学技術大学院大学情報科学研究科 Graduate School of Information Science, Japan Advanced Institute of Science and Technology |
| 発表年月日 | 1999/11/12 |
| 資料番号 | KBSE99-41 |
| 巻番号（vol） | vol.99 |
| 号番号（no） | 426 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |