6章振る舞い仕様を検査する

6.1 状態遷移システム

6.1.1 状態遷移マシン

Mealyダイアグラムで表現する

P.127下～

（状態，入力，遷移関数，初期状態，終了状態）

P.128上～

プログラムでも（だいたいは）表現できる

6.1.2 述語論理による解釈

(1) 厳密な表現の目的

プログラムによる表現では網羅性の高い検査ができない

P.128下～

述語論理で表現すれば検査が可能

(2) 決定性有限状態オートマトン

DFA(Deterministic Finite-State Automaton): Mealyより単純

P.129下～

蛍光灯と思えばよい

定義通り表現してもやはり，網羅性の高い検査ができない

（入力パターンを与えないと何も分からない）

[ex10-1] 状態遷移システムに無関係なものはどれですか

[ex10-3] 状態遷移システムを（プログラムなどの）実行可能な形式で表現した場合の問題はどれですか

(3) 系列の表現

網羅性の高い検査を可能にするために，シーケンスを用いる

シーケンス

リストみたいなもの

非反射的(irreflexible)

推移的(trasitive)

全域的(total)

P.130下～

nextが無い＝終端

P.131上～

noDense: 実数でなく整数，という感じ

マーク付きシーケンス

ItemとMarkerを交互に

DFAの解釈

initInterval: 前にItemの無Marker

ends(e,v): vはeで終わる

begins(e,v): vはeで始まる

P.133上～

初期値
pressとfinishは違う
isOffからfinishの遷移はない
isOn --press--> isOff
pressもfinishも起こらなければそのままの状態

P.134上～

この表現なら論理式を用いて検査できる

6.1.3 UMLステート図

省略

[ex10-4] 時間の流れに伴なう状態遷移を表すためのシーケンスについて、不要な性質はどれですか

[ex10-5] 状態遷移列を表すシーケンスで使われるItemとMarkerの2つは何と何を表していますか

[ex10-6] 状態遷移を実行可能な形式で表現するときには不要で、述語で表現するときに必要となるのはどれですか

課題

教科書（図はすべてこちらより引用）：
　中島震，「形式手法入門―ロジックによるソフトウェア設計―」，オーム社

一覧に戻る

6章 振る舞い仕様を検査する