モデルの記述と検証のためのプログラミング入門


タイトル モデルの記述と検証のためのプログラミング入門
著者 二木 厚吉
出版社 株式会社サイエンス社
正誤表 iprog-seigo.pdf (2018-8-7)

コードダウンロード

注意 WindowsとMac/Unixのコードのエンコーディングが異なるので、必ず自分のシステムに対応してるコードをダウンロードください:

Windows Download Mac/Linux Download
cafeobjCodes-Windows.zip cafeobjCodes-Unix.zip

ダウンロードしたファイルcafeobjCodes.zipを解凍すると, cafeobjCodesというディレクトリ(directory)が得られる. cafeobjCodesには,4つのCafeOBJファイル chap1.cafe, chap2.cafe, chap3.cafe, chap4.cafeと, 24のCafeOBJファイルを含むディレクトリchap5が含まれる.

練習問題の解答例はすべて上記の4+24のCafeOBJファイルの 対応する部分に記載されている.

CafeOBJの現ディレクトリ(current directory)をcafeobjCodesとし,inputコ マンド:

 input chap1.cafe
 input chap2.cafe
 input chap3.cafe
 input chap4.cafe

のいずれかでCafeOBJファイルを読み込ませると, 対応する章のCafeOBJコードがすべて実行され,すべてのモジュール定義が読み込まれる.

CafeOBJの現ディレクトリをchap5とし,inputコマンド:

 input chap5.cafe

でCafeOBJファイルを読み込ませると, ディレクトリchap5の24のファイルに入っている5章のすべてCafeOBJコードが実行され, すべてのモジュール定義が読み込まれる.

本書に掲載されているCafeOBJコードの振る舞いを部分的に確認するには, CafeOBJシステムを起動した直後の初期状態で, 上記の5つのinputコマンドのいずれかにより 振る舞いを確認したいコードに関連するモジュールの 定義をすべて読み込んでから, 動作を確認したいコードを実行するのが良い.

すでに定義(CafeOBJ仕様)が読み込まれているモジュールと同じモジュール 名をもつモジュール定義を読み込ませると,システムは

 [Warning]: Redefining module [module-name] done.

と表示して,モジュール[module-name]の定義を新たに読み込んだもので上書きする. モジュールの定義を上書きすると,そのモジュールをサブモジュールとする モジュールに不整合を生じさせる恐れがあり,十分に注意する必要がある.

CafeOBJシステムは

https://cafeobj.org/download/からダウンロードできる(CafeOBJ-1.5.6以降のバージョンを使用すること).