抽象によるソフトウェア設計 第6章 事例 その8

今日は 6.4.6 履歴変数からです。

• 固定サイズメモリモデルの抽象モデル準拠の証明はそのままだとできない。固定モデルは初期状態から全てのアドレスが任意の初期値への対応を持つため
  • unwritten という「既にそのアドレスに書き込みされたか」というフィールドをもたせるモデルに拡張することで抽象モデルに準拠させることができる。このような要素を「履歴変数」と呼ぶ

これで本文は終わりです。しかしここから長い付録が続くので適当に気の向いたものを解きながら進めていきたいと思います。