| 講演名 | 2004/1/16 コンポーネントインタフェースにおける契約デザインの整合性検証 蔭山 達也, 丸山 勝久, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | コンポーネントへのデータの入出力に関する仕様を契約デザイン(Design by Contract)内の事前条件と事後条件で表現することで,コンポーネント利用者に対して有益な情報を公開できる.しかしながら,これらの条件間に整合性がなければ,不適切な情報を公開することになる.そこで,本稿では,これらの条件間の整合性を効率的に検証する手法を提案する.ここでは,プログラムの実装が正しいという前提のもとで,事前条件が正しいときに事後条件は正しいかどうかを確認することを,整合性検証と定義する.本手法では,Conditioned Slicingを用いてコンポーネントの入出力に関係のある文のみを抽出することで,整合性検証のコストをより低く抑えることが可能である. |
| 抄録(英) | Pre- and post-conditions in "Design by Contract" are useful for helping component users understand the specification about input- and output-data of components. However, these conditions in existing software are not always consistent with its implementation since they are often written after developing the source code or individually modified by different developers. This paper proposes a method for checking the consistency between pre- and post-conditions on the assumption that the pre-condition and implementation are correct. To reduce the cost of validation, the proposed method uses Conditioned Slicing which is a technique 'For extracting only statements related to input- and output-data. |
| キーワード(和) | コンポーネント / 契約デザイン / プログラムスライス / Conditioned Slice / 記号実行 / 整合性検証 |
| キーワード(英) | Component / Design by Contract / Program Slice / Conditioned Slice / Symbolic Execution / Validation |
| 資料番号 | SS2003-43 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2004/1/16(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | コンポーネントインタフェースにおける契約デザインの整合性検証 |
| サブタイトル（和） | |
| タイトル（英） | Consistency Check for Pre- and Post-Conditions of "Design by Contract" in Component Interfaces |
| サブタイトル（和） | |
| キーワード(1)（和/英） | コンポーネント / Component |
| キーワード(2)（和/英） | 契約デザイン / Design by Contract |
| キーワード(3)（和/英） | プログラムスライス / Program Slice |
| キーワード(4)（和/英） | Conditioned Slice / Conditioned Slice |
| キーワード(5)（和/英） | 記号実行 / Symbolic Execution |
| キーワード(6)（和/英） | 整合性検証 / Validation |
| 第 1 著者 氏名（和/英） | 蔭山 達也 / Tatsuya KAGEYAMA |
| 第 1 著者 所属（和/英） | 立命館大学大学院理工学研究科 Graduate school of Computer Science, Ritsumeikan University |
| 第 2 著者 氏名（和/英） | 丸山 勝久 / Katsuhisa MARUYAMA |
| 第 2 著者 所属（和/英） | 立命館大学理工学部情報学科 Department of Computer Science, Ritsumeikan University |
| 発表年月日 | 2004/1/16 |
| 資料番号 | SS2003-43 |
| 巻番号（vol） | vol.103 |
| 号番号（no） | 583 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |