Contents of Report

[Data of Report]

Report Number:: TR0853
Date of Registration:: 1993.08
English Title:: ***
Japanese Title:: Metis-AS における代数的仕様の検証手続き
English Author:: A.Osuga,K.Sakai,S.Honiden
Japanese:: 大須賀　明彦,坂井　公,本位田　真一
Name of Organization to which author belongs:: Toshiba,Tuskuba Univ.,Toshiba
PDF:: tr0853.pdf

[Contents]

	要旨	.... 2
1	はじめに	.... 2
2	準備	.... 3
3	項書換え技術	.... 4
4	基本検証手続き	.... 5
5	無限実行への対処	.... 8
5.1	包含処理の導入	.... 8
5.2	再帰対による無限実行の検出	.... 8
5.3	無限実行を回避する要対の選択	.... 9
5.4	再帰対を簡約する補題の追加	.... 10
5.5	その他の方法	.... 11
6	手続きの改良	.... 11
6.1	入力条件を満たさない仕様への対処	.... 11
6.2	冗長な定理の除去による効率化	.... 12
6.3	等式の分配による手続きの効率化	.... 12
6.4	証明済規則の導入による能力の向上	.... 12
6.5	誤りを含む部分仕様の提示	.... 13
6.6	改良された検証手続き	.... 13
7	検証例	.... 14
7.1	自然数の加算の検証	.... 14
7.2	エレベータボタン操作の仕様検証	.... 14
8	おわりに	.... 17
9	謝辞	.... 18
10	参考文献	.... 18
	End	.... 19

目次をクリックすると、PDFファイルが表示されます。

ICOT研究論文（TR）一覧に戻る / Back to the list of ICOT Technical Reports