i217 関数プログラミング第 13 回プログラム検証 2 二木厚吉 緒方和博 計算機による検証支援 SML のプログラム ( 関数 ) の性質を帰納法等により明らかにすることは可能である. つまり プログラムを検証 ( プログラムが望ましい性質を満たすことを証明 ) することは可能である. ただし SML の処理系は 検証 ( あるいは証明 ) を支援しない. 検証を支援するための計算機言語やツールがある. CafeOBJ はそのような言語 / ツールの 1 つである. CafeOBJ は,JAIST を中心に開発された, 計算機システム ( プログラム等 ) の要求仕様や設計仕様を書くための計算機言語で, 要求仕様や設計仕様が望ましい性質を満たすことの検証を支援するツールでもある. 2
CafeOBJ に関するページ CafeOBJ official homepage: http://www.ldl.jaist.ac.jp/cafeobj/ CafeOBJ の入手先 : http://www.ldl.jaist.ac.jp/cafeobj/system.html 本学の計算機環境にもインストール済 /pkg/all/bin/cafeobj CafeOBJ 入門 : http://www.jaist.ac.jp/~t-seino/lectures/cafeobj-intro-j/ 3 CafeOBJ の起動 CafeOBJ を起動するとバージョン等の情報に引続き プロンプト CafeOBJ> が表示される. > cafeobj -- loading standard prelude ; Loading c: cafeobj prelude std.bin CafeOBJ> -- CafeOBJ system Version 1.4.6(PigNose0.99,p5) -- built: 2005 Nov 22 Tue 7:00:04 GMT prelude file: std.bin *** 2007 Oct 25 Thu 1:16:05 GMT Type? for help *** -- Containing PigNose Extensions -- --- built on Allegro CL Enterprise Edition 6.2 [Windows] (Nov 22, 2005 15:59) 4
CafeOBJ の終了 コマンド quit で終了する. CafeOBJ> quit [Leaving CafeOBJ] ; Exiting > 異常状態からは :q で復帰できることがある. ( 特に windows 上の emacs において有効 ) 5 モジュール CafeOBJ 文書 ( 仕様 ) の基本単位はモジュールである. モジュールの例 : mod! PNAT+ { [Pnat] op zero : -> Pnat op s : Pnat -> Pnat op _+_ : Pnat Pnat -> Pnat {l-assoc prec: 40} vars X Y : Pnat eq X + zero = X. eq X + s(y) = s(x + Y). } モジュールの基本形は mod! ModName { } である. に ソート 演算子 ( 関数 ) 変数および等式が宣言される. 6
ソート宣言 ソートは ものの集まりを表しており, プログラミング言語における型に相当する概念である. ブラケット ([ と ]) で囲って宣言する. [SortName 1 SortName 2 SortName n ] モジュール PNAT では : [Pnat] ソート ( 名 )Pnat が宣言されている. Pnat はすべての自然数の集まりを表している. 7 演算子宣言 (1) ソート ( ものの集まり ) の上の関数の型情報 (SML の関数の仕様 ) に相当するものを宣言する. 演算子宣言の基本形 : op fname : Sort 1 Sort n -> Sort : と -> の間にあるソート列をこの演算子のアリティ (arity) と呼ぶ. -> の右のソートをこの演算子のコアリティ ( あるいはソート ) と呼ぶ. アリティとコアリティの 2 つを, この演算子のランク (rank) と呼ぶ. 式 ( 項 )fname(t 1,,t n ) のソートは Sort である. ただし,t 1,,t n は,Sort 1,,Sort n の項 ( 値や式 ) である. 同じランクの演算子を複数同時に宣言する場合,op ではなく,ops を用いる. ops f 1 f m : Sort 1 Sort n -> Sort ソート宣言と演算子宣言をあわせて, モジュールのシグネチャ (signature) と呼ぶ. 8
演算子宣言 (2) モジュール PNAT では : op zero : -> Pnat op s : Pnat -> Pnat op _+_ : Pnat Pnat -> Pnat {l-assoc prec: 40} _+_ 演算子は中置記法で使われ, 左結合で, 結合度 40 を持つ. l-assoc が _+_ は左結合 (a + b + c は (a + b) + c のこと ) であることを指定する. Pnat の項は以下のようなものである. zero, s(zero), s(s(zero)), zero + zero, s(zero) + zeor, zero + s(zero),s(zero) + s(zero), Pnat は, このような項の集まりを表す. zero は自然数の 0,s は後者関数 (+1),_+_ は自然数の加算を表す. 9 変数宣言 変数宣言の基本形 : var vname : Sort 変数 vnameは, ソートSortの任意の項を現す. 等式で用いる. 同じソートの変数を複数同時に宣言する場合,varではなく, varsを用いる. vars v 1 v n : Sort モジュールPNATでの例 : vars X Y : Pnat 10
等式宣言 (1) 演算子の定義や性質を記述する. 等式宣言の基本形 : eq term 1 = term 2. term 1 は, 変数以外の項である. term 2 に含まれる変数は,term 1 にも含まれていなければならない. 最後は, 必ずフルストップ ( ピリオド ). で終わらなければならない, ことに注意. モジュールに宣言される等式は, そのモジュールの公理とも呼ばれる. 11 等式宣言 (2) モジュール PNAT での例 : eq X + zero = X. eq X + s(y) = s(x + Y). この 2 つの等式で, 演算子 _+_( 自然数の加算 ) を定義している. 12
コマンド open と close コマンド open でモジュールを開き, モジュール内に宣言されているソート, 演算子, 変数および等式を利用可能にする. CafeOBJ> open PNAT+ -- opening module PNAT.. done. %PNAT+> コマンド close で, 開いたモジュールを閉じる. %PNAT+> close CafeOBJ> select モジュール名 または auto context on を使う方法もある. 13 コマンド parse(1) 入力したものが正規の項であるかどうか判定し, 正規のものであれば, その項のソートを含めた情報を返す. %PNAT+> parse s(s(zero)) + zero. (s(s(zero)) + zero) : Pnat 正規のものでなければ, エラーメッセージを返す. %PNAT+> parse s(s(zero)) + zoro. [Error] no successfull parse parsed:[ s(s(zero)) ], rest:[ (+ zoro) ] (parsed:[ s(s(zero)) ], rest:[ ("+" "zoro") ]) : SyntaxErr + の前後には ( 基本的に ) スペースが必要である. 14
コマンド parse(2) verbose( 多弁 ) モードを on にすることで, 項の構文木を表示するようになる. %PNAT+> set verbose on %PNAT+> parse s(s(zero)) + zero. (s(s(zero)) + zero) : Pnat _+_:Pnat / s:pnat zero:pnat s:pnat zero:pnat 15 コマンド red 式 ( 項 ) を計算する. 等式を左から右への書換え規則とみなし, 項を書換える ( 簡約する ). %PNAT+> red s(s(zero)) + zero. -- reduce in %PNAT : s(s(zero)) + zero s(s(zero)) : Pnat (0.000 sec for parse, 1 rewrites(0.000 sec), 1 matches) %PNAT+> red s(s(zero)) + s(s(zero)). -- reduce in %PNAT : s(s(zero)) + s(s(zero)) s(s(s(s(zero)))) : Pnat (0.000 sec for parse, 3 rewrites(0.000 sec), 5 matches) 16
自然数の乗算 モジュールPNAT+ に以下の演算子宣言を加える. op _*_ : Pnat Pnat -> Pnat {l-assoc prec: 30} prec: nは結合度を指定. nが小さいほど結合力は大きい. _+_ の結合度は40であった. この演算子を定義する等式を宣言する. eq X * zero = zero. eq X * s(y) = (X * Y) + X. 得られたモジュールを PNAT* とする. 17 階乗の計算 モジュール PNAT* に以下の演算子宣言を加える. op fact1 : Pnat -> Pnat op fact2 : Pnat -> Pnat op sf2 : Pnat Pnat -> Pnat これらの演算子を定義する等式を宣言する. eq fact1(zero) = s(zero). eq fact1(s(x)) = fact1(x) * s(x). eq fact2(x) = sf2(x,s(zero)). eq sf2(zero,y) = Y. eq sf2(s(x),y) = sf2(x,s(x) * Y). 得られたモジュールを FACT とする. 18
等価判定の演算子 モジュール FACT に以下の演算子宣言を加える. op _=_ : Pnat Pnat -> Bool {comm} Bool はブール値 ( の集まり ) を表すソートである. {comm} は 演算子 _=_ が交換律を満たすことを指示している (m = n であれば n = m). この演算子を定義する等式を宣言する. eq (X = X) = true. eq (zero = s(x)) = false. eq (s(x) = s(y)) = (X = Y). 得られたモジュールを FACT= とする. 19 パラメタ付モジュール モジュールはパラメタを持てる. 例 ( 汎用のリストのモジュール ): mod! LIST (M :: EQTRIV) { } M がこのモジュールの仮パラメタである. 実パラメタは モジュール EQTRIV に記述されている要件を満たす必要がある. モジュール EQTRIV は以下のとおり. mod* EQTRIV { [Elt] op _=_ : Elt Elt -> Bool } 要件とは, 実パラメタのモジュールは少なくとも Elt に対応するソートと _=_ に対応する演算子を有する, ということである. モジュール PNAT はこの要件を満たす. 20
モジュール LIST のシグネチャ [List] op nil : -> List op _::_ : Elt.M List -> List op _@_ : List List -> List {assoc} op _=_ : List List -> Bool {comm} op rev1 : List -> List op rev2 : List -> List op ar2 : List List -> List {assoc} は, 演算子 _@_ が結合律 ((a @ b) @ c と a @ (b @ c) は同じ ) を満たすことを指定する. 21 モジュール LIST の公理 eq (L = L) = true. eq (nil = (X :: L)) = false. eq ((X :: L) = (Y :: L1)) = (X = Y) and (L = L1). eq nil @ L = L. eq (X :: L1) @ L = X :: (L1 @ L). eq rev1(nil) = nil. eq rev1(x :: L) = rev1(l) @ (X :: nil). eq rev2(l) = ar2(l,nil). eq ar2(nil,l) = L. eq ar2(x :: L1,L) = ar2(l1,x :: L). 22
練習問題 1. モジュール FACT= に, 自然数 n を与えると総和 (1+ +n) を表す演算子 sum を宣言し, 総和を再帰的に計算する等式 (sum を定義する等式 ) を追加して, モジュール SUM を定義せよ. 2. モジュール LITS に リスト l を引数に与えると l の長さ ( 要素数 ) を表す演算子 length の宣言と, 長さを再帰的に計算する等式 (length を定義する等式 ) を追加し, モジュール LISTlen を定義せよ. ヒント : モジュール LISTlen はモジュール SUM を輸入する必要がある. このためには モジュール LISTlen に protecting(sum) or pr(sum) を以下を追加する. 23