振舞意味論を用いた詳細化検証 : オブジェクト合成と非観測射影演算を用いた新しいアプローチ  [in Japanese] Refinement by using Behavioral Semantics : The new approach which uses object composition and non-observable projection operators  [in Japanese]

振舞意味論は, 対象とするソフトウェアをブラックボックスと見なし, 観測される振舞いでソフトウェアをモデル化する手法である. 観測結果でソフトウェアの状態を区別するというアイデアにより, 従来, 人間が自然に行っていた, 意識したくない部分は無視して, 意識したい部分のみをモデル化するという行為を, フォーマル化している. ソフトウェア開発の工程では, 抽象的な仕様をまず記述し, それを基に徐々に具体的な仕様を記述し, 最終的に実装を行う. この時, これらの仕様間には, (対象とするソフトウェアの)意識したい部分が増加しているという関係がなければならない. この関係を検証するのが詳細化検証である. なお, 意識したい部分のみをモデル化するという行為をフォーマル化することで, 詳細化検証を項書換えシステムを用い, 計算機支援の下, 厳密に実行することが可能になる. 本稿では, このフォーマル化の手法として, オブジェクト合成と非観測射影演算を用いる手法を提案する. なお, この手法の利点は, 従来の方法に比べ, 検証の自動化可能な部分が増加することである.

Behavioral semantics is a methodology that the target software is regarded as a black box. By the idea that the states of the software are determined by experiments, the action that the things we want to ignore are ignored is formalized. In the software development process, we specify many specifications whose levels are from abstract level to concrete level. In these specifications, there must be the relation that models of a concrete level specification must satisfy an abstract level specification. Verification of this relation is refinement. By using specifications based on behavioral semantics, we can verify refinement on term rewriting based reducers. In this paper, we propose the formalization method which uses object composition and non-observable projection operators. The advantage of this method is that the part which can be verified automatically increases.