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

今日は 6.4.4 抽象化関数の簡単な紹介からです。

  • 具体的なメモリモデルから抽象的なモデルの関連付け
    • 具体的なモデルでの操作が抽象的なモデルの操作に対応していることを示す
  • 抽象化関数
    • 具体的なモデルでの状態を抽象的なモデルの状態に対応付ける関数(alpha)を導入
    • concreteOp [s, s'] => abstractOp [alpha [s], alpha [s']]
      • となるような alpha が定義できれば、具体的モデルの振舞いは抽象モデルに準拠(conform)すると言う
      • 「状態」そのものは見えないものとして振舞いが一致していればよい
  • この手法は健全(sound)なので抽象化関数がみつかれば必ず具体的機械は抽象的機械に準拠するが、完全(complete)ではないので準拠するけど抽象化関数が存在しない可能性がある
    • 具体的モデルを拡張することで解決できる
  • 抽象化関数は全域である必要がある
  • キャッシュメモリのモデルについて抽象化メモリモデルへの準拠をチェック
    • 別々のファイルに記述してあるので open で取り込む。操作述語名が衝突しているので as で別名つきで取り込んで操作に prefix をつける
    • load, flush など具体的モデルにしか存在しない操作は抽象化モデルの「何もしない」そうさに対応する(抽象的状態が変化しない)ことを確認する

あとは第6章は抽象化関数がみつからない時のための履歴変数の導入についてだけです。