Pipeline と PathFinder
MenuMercural ssh:/net/home/hg/teacher/kono/os/ex/WorkerModel1
を実行してみて、Pipeline 実行の様子を調べよ。
Pipeline の例題がきちんと停止することを Java PathFinder を使って確認せよ。
まず、きちんと停止することを確認する assert を考える。
jpf で実行してみる。
停止しないプログラムを作成して、assert が失敗することを確認せよ。
停止するプログラムを作成して、assert が成功することを確認せよ。
これは、プログラムがちゃんと動くことの保証になっているか?