オートマトンと双代数の現実的な意味と例
次の3者の関係が問題
- 仕様と仕様の記述方法
- 仕様に基づいて実装する“実装者”
- 実装が仕様に合致しているかどうかを確認する“テスター”
次のように考える。
- 仕様は、モノイド生成元と関係で与えられる。関係には観測演算子が使われる。
- テストには、テスト式と期待表明（エクスペくテーション）とテスト結果が使われる。
- 実装者は内部構造を知っている。
- テスターは内部構造を知らない。
あるいは、
- 仕様は指標と公理系
- 実装はモデル
- テスターは論理を使う
例は、いつものヤツ
- トグルボタン（toggle, isOn）
- カウンター（up, down, value）
- 危ない自然数スタック（empty状態でpopすると壊れる）
- ab* の認識器（{a, b}* が作用して、状態空間は {0, 1, ⊥}）
注意事項
