http://d.hatena.ne.jp/a-san/20090729#p1 VDMのmeasure関数の定義の仕方が少しずつわかってきました。 measure関数の引数は、元の関数の引数と一致しなければならない。 measure関数の戻り値は、nat、または natのタプルでなければならない。 再帰関数が以…