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

今年最初の朝読書です。今年はもうちょっと多く読めるといいなぁ。

今日は 6.4 メモリの抽象化のところからです。

• メモリを Addr と Data のアトムの対応付けとしてモデル化する
  • パラメータ付きモジュールにして Addr, Data のシグネチャはパラメータとして受け取るようにしている
  • メモリの読み書きを述語(pred)として宣言しているが read は引数の Data がメモリ内容と一致するという制約を宣言することで読み込みしている。ちょっとおもしろい(慣れないと関数として書いてしまいそう)
• キャッシュメモリ付きのモデル
  • キャッシュのフラッシュをread/write とは分離して宣言していてキャッシュポリシーは別に定義するようにしている
  • キャッシュのアドレスが主メモリのアドレス内に収まるように値域指定演算子を利用
• 固定サイズメモリ
  • もう少し現実的にサイズが固定されているメモリ
  • 述語 init はインタフェースの統一のためか宣言されているけど空っぽ
  • 任意の値で初期化されている、ということは data フィールドの Data の多重度を lone から one にしておいて特に何も宣言しなければよい

今日の内容は3つのメモリモデルを作ったところまでですが、続いてはこれを抽象化して包括的なモデルの検証をするようです。