2008-05-10 - 梶本裕介の日記

の時， int r = 1; for (int i = 1; i が実行さらた際に，となることを示す（簡単化のために値の定義域は無視する）．まず，このループのloop invariant は，である．これを示すには，を証明すればよい．代入列がを真に定めて停止するweakest preconditionはなので，を示す．．次に，ループが停止すること，つまり，を示す．これには残りの繰り返し回数の上界を表す上界関数を示せば十分であり，これはである．ここで，新しい変数に対し，だから，であり，は繰り返しのたびに減少し，また，より，だから，は繰り返しが残っているときは0より大きい．以上より，であることが言えた．次に，なら，ループの開始前にが真であること，つまり，を示す．．最後に，がより弱いこと，つまりを示す．．これでちゃんと階乗が計算できることが示された．多分！