|
目次
第１節 繰り返し
第２節 繰り返しからのブレークアウト
テスト
Logをみる
Back
|
第７章 ソフトウェアの論理モデルⅡ 第２節 繰り返しからのブレークアウト
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は繰り返し部から飛び出す直前に実行される文です。ｂｒｅａｋの機能の欠点はfor文の次の文にループからジャンプして来るため、制御変数 i がnまで行って正常にループが終了した場合と区別がつかないことです。breakの直前に実行されるstatement_bの中でbflagのようなフラグ変数を１にする、という方法もあります。そうすればfor文の次の文の中でbflagの値をみればbreakして出てきたのか、正常に終了して出てきたのかの区別がつきます。
あるいは制御変数が正常に抜けたときはi=n+1となっているはず（ｂｒｅａｋしたときはｂｒｅａｋしたときの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;
となります。ちょっと複雑そうですが理に適った論理モデルです。
例１ 次のプログラムは１９６７７の約数のうち最小のものを探すものである。約数は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が１９６７７の（１を除いた）最小の約数となることを示せ。
解） 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;
|