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

 第1節 繰り返し

目次


第1節 繰り返し

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


テスト

Logをみる

Back
 

第7章 ソフトウェアの論理モデルU 第1節 繰り返し

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

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

 繰り返しについては、

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

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

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

 ですから、

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

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

例1 整数1〜nまでの和を変数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;

となります。これを実際Mizarの定理として証明してみましょう。

 5章3節に現れたnビットカウンタのときの証明と同じく数学的帰納法を使って証明します。複雑そうに見えるのはk+1がnより大きくなるときとかの例外処理があるからです。本質的には高校の数学レベルの話です。i や n をInteger型とせずNat型としたのはs/.iがInteger型として計算できるためです。以後プログラム中のint型はMizarの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;