目次

　第２節　繰り返しからのブレークアウト

テスト

Logをみる

Back
　

　前章で述べたのは繰り返し部の無いプログラムについてです。プログラムの中ではfor文やrepeat until文やdo while 文などが繰り返しのために用意されています。あるいは構造化プログラムでは禁止されているif goto を使う方法でも繰り返しは実現されます。　繰り返しのときはどんな方法を取るにしてもどうしても何か繰り返しを制御する変数が必要で、それに対しては上書きをしなければならないのです。

　それでは上書きをしない、という前提が崩れてしまいますので、繰り返しについては次のように考えます。

　繰り返しについては、

　for (i=m;i<=n;i++){   } 

という形だけを許す、というものです。i++というのはi=i+1という上書きのしるしですが、そう考えずに、m<=i<=n を満たすすべての自然数、あるいは整数について｛　｝がいえる、と解釈するのです。ですからfor は繰り返しではなく、全称記号である、と考えるのです。i はそのときの束縛変数です。ですから、まさにＭｉｚａｒのfor と同じ考えです。

　勿論プログラムですから、演算順序はあります。演算順序はm,m+1,m+2,...,n と実行するものとします。この演算順序は、「{ }の中で初めて現れた変数が、いきなり右辺にくることはない。まずあらかじめ１回だけ左辺に現れる必要がある」という上書き禁止の規範をチェックするためだけに必要なものです。

　ですから、

　for (i=n;i<=m;i--){   } 

としても論理モデルとしては同じですが、上書き禁止の規範のチェックがクリアするかが問題となります。クリアしていればこの書き方でもいいのです。

例１　整数１〜ｎまでの和を変数d　に求める次のプログラムの正しさを証明せよ。

int s[10001],d,i;
s[1]=0;
for (i=1;i<=n;i++){s[i+1]=s[i]+i;}
d=s[n+1];

解）これの論理モデルは

reserve s for FinSequence of INT,d for Integer,n for Nat;
theorem n>=1 & len s=10000 & s/.1=0 & 
(for i being Nat st 1<=i & i<=n holds s/.(i+1)=s/.i +i)
      & d=s/.(n+1) implies d=n*(n+1)/2;

となります。これを実際Ｍｉｚａｒの定理として証明してみましょう。

　５章３節に現れたｎビットカウンタのときの証明と同じく数学的帰納法を使って証明します。複雑そうに見えるのはｋ＋１がｎより大きくなるときとかの例外処理があるからです。本質的には高校の数学レベルの話です。i や　n　をＩｎｔｅｇｅｒ型とせずＮａｔ型としたのはs/.iがＩｎｔｅｇｅｒ型として計算できるためです。以後プログラム中のｉｎｔ型はＭｉｚａｒのInteger型になったりNat型になったりしますが、負にならないことが分かっているときはどちらに対応させてもいいのです。

environ
 vocabulary ARYTM_3,INT_1,FINSEQ_1,FINSEQ_4;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
   XREAL_0, REAL_1,NAT_1,INT_1,FINSEQ_1,FINSEQ_4;
 constructors REAL_1, XREAL_0, XCMPLX_0, XBOOLE_0,NAT_1,INT_1,
   FINSEQ_1,FINSEQ_4;
 clusters REAL_1, NUMBERS, ORDINAL2, XREAL_0, XBOOLE_0, NAT_1,INT_1,
   FINSEQ_1 ,RELSET_1;
 schemes NAT_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 theorems AXIOMS,NAT_1;

begin
reserve s for FinSequence of INT,d for Integer,n for Nat;

theorem n>=1 & len s =10000 & s/.1=0 &
(for i being Nat st 1<=i & i<=n holds s/.(i+1)=s/.i +i)
      & d=s/.(n+1) implies d=n*(n+1)/2
proof assume A0: n>=1 & len s =10000 & s/.1=0 &
  (for i being Nat st 1<=i & i<=n holds s/.(i+1)=s/.i +i)
      & d=s/.(n+1);
  defpred P[Nat] means $1<=n &
  (for i being Nat st 1<=i & i<=n & i<=$1 holds s/.(i+1)=s/.i +i)
       implies s/.($1+1)=$1*($1+1)/2;
  s/.1=0/2 by A0;then
  0<=n &
  (for i being Nat st 1<=i & i<=n & i<=0 holds s/.(i+1)=s/.i +i)
       implies s/.(0+1)=0*(0+1)/2;then
 A2: P[0];
 A3: for k being Nat st P[k] holds P[k+1]
  proof let k be Nat;
   assume P[k];then
    B2: k<=n &
    (for i being Nat st 1<=i & i<=n & i<=k holds s/.(i+1)=s/.i +i)
       implies s/.(k+1)=k*(k+1)/2;
    B3: for i being Nat st 1<=i & i<=n & i<=k holds s/.(i+1)=s/.i +i
                       by A0;
    now per cases;
    case C0: k+1<=n;
      kn;
      hence P[k+1];
     end;
     end;
    hence P[k+1];
   end;
  for k being Nat holds P[k] from NAT_1:sch 1(A2,A3);then
  P[n];then
  (for i being Nat st 1<=i & i<=n & i<=n holds s/.(i+1)=s/.i +i)
        implies s/.(n+1)=n*(n+1)/2;then
  s/.(n+1)=n*(n+1)/2 by A0;
 hence d=n*(n+1)/2 by A0;
end;