情報証明論 第7章 ソフトウェアの論理モデルU

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

目次


第1節 繰り返し

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


テスト

Logをみる

Back
 

第7章 ソフトウェアの論理モデルU 第2節 繰り返しからのブレークアウト

 for文は基本的には制御変数i の終値まで実行されることを想定しています。しかしrepeat untilやdo whileはある条件が成立すると(あるいは成立しなくなると)ループの中から抜けることを想定しています。ループの回数は不定です。

 これはきれいなプログラムのようですが、条件によっては無限回か、それに近い回数の繰り返し処理が行われる恐れがあります。

 メモリをどの位とるか分からないような処理、演算を何回やるか分からないような処理、はなるべく避けた方がいいのです。お客がいつになく増えたとき、突然ストップしてしまう業務用コンピュータシステムはそのようなものでしょう。

 むしろ繰り返しの最大数を決めておき、その範囲に収まるよう入力に何らかの方法で制限を加えた方がいいのです。あるいは制限回数を越えたらエラー表示をし、それより先に処理が進まないようにすることもよいでしょう。

 そのような安全な繰り返しからのブレークアウトは次のようなプログラムです。

for (i=m;i<=n;i++){statement_1;statement_2;...;if (statement_f){statement_b1;...;break;}}

statement_fがブレークするための条件です。statement_bは繰り返し部から飛び出す直前に実行される文です。breakの機能の欠点はfor文の次の文にループからジャンプして来るため、制御変数 i がnまで行って正常にループが終了した場合と区別がつかないことです。breakの直前に実行されるstatement_bの中でbflagのようなフラグ変数を1にする、という方法もあります。そうすればfor文の次の文の中でbflagの値をみればbreakして出てきたのか、正常に終了して出てきたのかの区別がつきます。

 あるいは制御変数が正常に抜けたときはi=n+1となっているはず(breakしたときはbreakしたときのi の値。それはn 以下)ですので、それで区別できます。

 しかしいずれの方法も上書きをともなうため問題があります。制御変数は上書きを認める、と言いましたが、ループの外でその値を使うのは問題があるのです。

 そこで

for (i=m;i<=n;i++){statement_1;statement_2;...;if (statement_f){statement_b1;...;iwork=i;break;}else {if (i==n)iwork=n+1;}}

とすればiworkは上書きされることはなく(一度だけ書かれるだけ)、ループを抜けたあと、その値によって、どこで抜けたか、あるいはbreakせずに終了したか、を区別できます。ちょっと文が複雑になりますが、これを一つのパターンとして定めておけば、バグのないプログラムに近づけます。

 このときこれの論理モデルは

  (ex j being Integer st m<=j & j<=n &
                 (for i being Integer st m<=i & i< j holds
                  tr(statement_1 for i)& tr(statement_2 for i)&...
                                & not (statement_f for i))&
                 &tr(statement_1 for j)& tr(statement_2 for j)&...
                 &statement_f for j) &(statement_b for i)&...& iwork=j)
                or
                 (for i being Integer st 1<=i & i<=n holds
                  tr(statement_1 for i)& tr(statement_2 for i)&...
                                & not (statement_f for i))& iwork=n+1; 

となります。ちょっと複雑そうですが理に適った論理モデルです。

例1 次のプログラムは19677の約数のうち最小のものを探すものである。約数はiworkに入る。約数が無い場合はiwork=19677となる。

int i,iwork;
 for (i=3;i<=19676;i++){if (Int(19677/i)*i==19677){iwork=i;break}
         else{if (i==19677){iwork=19677;}}

  このプログラムの論理モデルを示し、それによるiworkが19677の(1を除いた)最小の約数となることを示せ。

解) breakのときの論理モデルの公式に従えば

           (ex j being Nat st 3<=j & j<=19676 &
                 (for i being Nat st 3<=i & i

となる。このとき、次のような定理とその証明が、iworkに最小の約数が入る、ということを示す。なお、環境部は無駄なものも含んでいる。

environ 
 vocabulary ARYTM_3,INT_1,FINSEQ_1,FINSEQ_4,NAT_1,ORDINAL2, ARYTM, ARYTM_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1,ORDINAL2, NUMBERS, XCMPLX_0,
   XREAL_0, REAL_1,INT_1,FINSEQ_1,FINSEQ_4,NAT_1;
 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, ARYTM_3, ZFMISC_1;
 schemes NAT_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 theorems AXIOMS,NAT_1,XCMPLX_1,INT_1,REAL_1,REAL_2;
begin

theorem
 for iwork being Nat st (
 (ex j being Nat st 3<=j & j<=19676 &
    (for i being Nat st 3<=i & i< j holds
      not (([\19677/i/])*i=19677))&
     (([\19677/j/])*j=19677) & iwork=j)
       or
      (for i being Nat st 3<=i & i<=19676 holds
     not (([\ 19677/i /])*i=19677))& iwork=19677)
   holds ex k being Nat st k*iwork=19677 &
     for m being Nat st 1< m & (ex s being Nat st m*s=19677) holds iwork<=m
 proof let iwork be Nat;
  assume A0: 
   (ex j being Nat st 3<=j & j<=19676 &
    (for i being Nat st 3<=i & i< j holds
      not (([\19677/i/])*i=19677))&
     (([\19677/j/])*j=19677) & iwork=j)
       or
      (for i being Nat st 3<=i & i<=19676 holds
     not (([\ 19677/i /])*i=19677))& iwork=19677;
   now per cases by A0;
   case 
     ex j being Nat st 3<=j & j<=19676 &
    (for i being Nat st 3<=i & i< j holds
      not (([\19677/i/])*i=19677))&
     (([\19677/j/])*j=19677) & iwork=j;then
     consider j being Nat such that
     C2: 3<=j & j<=19676 &
    (for i being Nat st 3<=i & i< j holds
      not (([\19677/i/])*i=19677))&
     (([\19677/j/])*j=19677) & iwork=j;
     C11: j>0 by C2,AXIOMS:22;then
     C10: 19677/j >0 by REAL_2:127;
     (([\19677/j/])*j/j=19677/j) by C2;then
     ([\19677/j/])=19677/j by C11,XCMPLX_1:90;then

     reconsider k2= [\19677/j/] as Nat by C10,INT_1:16;
     C9: k2*iwork=19677 by C2;
     for m being Nat st 1< m & (ex s being Nat st m*s=19677) holds iwork<=m
     proof let m be Nat;
      assume D1: 1< m & (ex s being Nat st m*s=19677);then
        consider s being Nat such that
        D2: m*s=19677;
        C2b: m*s+0=19677 by D2;
        m<>0 by D1;then
        19677/m=s by D2,XCMPLX_1:90;then
        C8: s= [\ 19677/m /] by INT_1:47;
        C4: 1+1<=m by D1,NAT_1:38;
         now assume D0: m=2;
           D2: 19677=2*9838 +1;
           D3: 19677 mod 2=0 by D0,C2b,NAT_1:def 2;
           19677 mod 2=1 by D2,NAT_1:def 2;
          hence contradiction by D3;
         end;then
         2< m by C4,REAL_1:def 5;then
         2+1<=m by NAT_1:38;
      hence iwork<=m by C2,C8,D2;
     end;
    hence ex k being Nat st k*iwork=19677 &
     for m being Nat st 1< m & (ex s being Nat st m*s=19677) holds iwork<=m
                       by C9;
   end;
   case C0:
      (for i being Nat st 3<=i & i<=19676 holds
     not (([\ 19677/i /])*i=19677))& iwork=19677;then
     B8: iwork=19677;
     B2: 1*19677=19677;
     for m being Nat st 1< m & (ex s being Nat st m*s=19677) holds iwork<=m
     proof let m be Nat;
      assume C1: 1< m & (ex s being Nat st m*s=19677);then
       consider s being Nat such that
       C2: m*s=19677;
       C2b: m*s+0=19677 by C2;
       now assume m< iwork;then
         m+1<=19677 by C0,NAT_1:38;then
         m+1<=19676 +1;then
         C6: m<=19676 by REAL_1:53;
         C4: 1+1<=m by C1,NAT_1:38;
         now assume D0: m=2;
           D2: 19677=2*9838 +1;
           D3: 19677 mod 2=0 by D0,C2b,NAT_1:def 2;
           19677 mod 2=1 by D2,NAT_1:def 2;
          hence contradiction by D3;
         end;then
         2< m by C4,REAL_1:def 5;then
         C5: 2+1<=m by NAT_1:38;
         C7: not m=0 by C1;
         19677/m=s by C2,C7,XCMPLX_1:90;then
         s= [\ 19677/m /] by INT_1:47;
        hence contradiction by C0,C5,C6,C2;
       end;
      hence iwork<=m;
     end;
    hence ex k being Nat st k*iwork=19677 &
     for m being Nat st 1< m & (ex s being Nat st m*s=19677) holds iwork<=m
                                        by B2,B8;
   end;
   end;
  hence ex k being Nat st k*iwork=19677 &
     for m being Nat st 1< m & (ex s being Nat st m*s=19677) holds iwork<=m;
 end;