関数プログラミング(I217

関数プログラミング(I217-1209)レポート問題
注意事項
1. 解答用の雛形ファイル 1209i217assignmentTemplate.cafe に対し，(1) …<n:Nat>
で示された部分（15+5+5+23=48 箇所）に適切な CafeOBJ コードを書き込み，(2) そ
れらに対し適切にコメントを付加して，解答ファイルを完成せよ．
2. !!! Tests !!!で示されるテストの記述（5 箇所）に含まれる全てのテストケースに
対して，-->で指定された式が出力されるように，CafeOBJ コードを書き込むこと．
3. 長いコメントを書く必要はないが，簡潔なコメントを適切な箇所に挿入することが推奨
される．コメントは，“{ コメント }” または ** コメント <end_of_line>のいず
れかのスタイル（雛形ファイルの最初の１０行を参照）を用いること．コメントは日本
語または英語で記述せよ．もし日本語コメントを含んだ解答ファイルを CafeOBJ システ
ムで適切に処理できなければ，コメント部分を別の pdf ファイルとして提出しても良い． 4. 解答ファイルの名前は<学籍番号＞<名字>-i217report.cafe とすること．たとえば
学 籍 番 号 が 1010034 で 名 前 が 鈴 木 一 郎 で あ れ ば ， 解 答 フ ァ イ ル の 名 前 を
1010034suzuki-i217report.cafe とせよ．日本語のコメントファイルを別ファイ
ルとして用意するときは，その名前は 1010034suzuki-i217report.pdf とせよ．
5. 解答ファイルの先頭には氏名(name)と学籍番号(student number)を記入すること．
6. 解答ファイル（.cafe ファイル）は，全ての指定部分に CafeOBJ コードを書き込んでな
く未完成でも，in コマンドを用いて CafeOBJ システムに読み込めるようにすること．
そのために，未完成の部分とそれに関係するテストケースをコメントとするなどの適切
な工夫をすること．
7. 解答ファイル（.cafe ファイル１つまたは.caf ファイルと.pdf ファイルの２つ）は〆切ま
でに，e-mail の添付ファイルとして， [email protected] 宛送ること．その e-mail
の件名（Subject）は i217-1209-report とすること．
[問題１] エラー処理を含むキューの定義（１5 点）
入れた順番でデータを取り出す（first in first out）データ構造キュウー（queue）を定義
せよ．関数 top の定義を参考にし，エラー処理が適切に定義されるように， enq 関数と deq
関数に対するランク（op 宣言）と等式（eq 宣言）を完成せよ． [問題２] テーブル関数の再定義（１５点）
講義資料４とその練習問題で示されたテーブルを操作する関数の定義（ans4.cafe ファイ
ルを参照）を以下のように再定義せよ．
1. insert を isKey と update を使って定義する．
2. remove を isKey と delete を使って定義する．
3. join を aKeyIn と merge を使って定義する．
ここで，(T1:Table aKeyIn T2:Table)は，テーブル T1 のキーの中にテーブル T2 のキーと
同じものが一つでもあれば true に，そうでなければ false になる．
[問題３] ３つのプロセスからなる Mutex の全状態遷移の定義（１５点）
３つのプロセス（p1,p2,p3）の相互排除プロトコル MUTEX（講義資料６参照）の任意
の N:Nat ステップまでの全ての状態遷移を，状態を要素とする３分無限木（3-ary infinite
tree）として定義せよ．また，それらの状態遷移に現れる状態が相互排除条件（mutual
exclusion condition）を満たすか否かを示す，真偽値（ture, false）を要素とする３分無限
木も定義せよ．
[問題４] ペアノ自然数に関する証明スコア（１５点）
ペアノ自然数の乗算（_*_）が望みの性質を満たすことを示す証明スコア（proof score）
完成せよ．ファイル中に示されている加算（_+_）に対する証明スコアを参考にせよ．