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

第2節 上書きをしないプログラム

目次


第1節 データ上書きの弊害と運命論

第2節 上書きをしないプログラム

第3節 条件分岐

第4節 プログラムの論理モデルと関数化


テスト

Logをみる

Back
 

第6章 ソフトウェアの論理モデルT 第2節 上書きをしないプログラム

 変数の上書きをしない、と決めてどの程度プログラムは書けるのでしょうか? 

例1 次のような処理のあるプログラムでは最終的に変数 d の値は何になるか?

  int a,b,c,d;
    a=6;
    b=a+7;
    c=b+3*a;
    a=a+b+c;
    d=3*a+b+c;

解)4行目で変数aに上書きされているので、新しい変数eを導入して次のように書き改める。

  int a,b,c,d,e;
    a=6;
    b=a+7;
    c=b+3*a;
    e=a+b+c;
    d=3*e+b+c;

するとこれは数学的な方程式と見ることができるから、

 d=3*e+b+c=3*(a+b+c)+b+b+3*a =3*(a+b+b+3*a)+2*b+3*a
   =3*a+6*b+9*a+2*b+3*a =15*a+8*(a+7)=15*6+8*13=90+104=194

すなわち194が答えである。

 194になるのはちょっとした暗算で出るので、上の例の解はおおげさすぎると思われるかもしれません。しかしとても発展的な考えが含まれているのです。

 上の例の解の中にあるプログラムは次のような論理命題に対応します。

a=6 & b=a+7 & c=b+3*a & e=a+b+c & d=3*e+b+c implies d=194;

これは論理命題なので前提の式の中でandで結ばれた式の順序は関係ありません。

c=b+3*a & e=a+b+c & d=3*e+b+c & a=6 & b=a+7 implies d=194; ...(1)

としても同じ命題式です。

 勿論最初のプログラムで行を矢鱈に変更することはできません。しかし上書きのないプログラムの場合、一度論理命題式に変換すると、そちらでは行を自由に入れ換え可能なのです。そして計算結果は変わらないのです。

 命題論理式がプログラムの代わりをするのです!

 それでは(1)式をMizarでチェックしてみましょう。環境部は似たような論文ファイルNAT_1のものを使い、notationなどにNAT_1自身を加えておきます。

environ
  vocabulary ORDINAL2, ARYTM, ARYTM_1, ARYTM_3, ORDINAL1, NAT_1, XREAL_0;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS, XCMPLX_0,
    XREAL_0, REAL_1,NAT_1;
 constructors REAL_1, XREAL_0, XCMPLX_0, XBOOLE_0,NAT_1;
 clusters REAL_1, NUMBERS, ORDINAL2, XREAL_0, ARYTM_3, ZFMISC_1, XBOOLE_0,
      NAT_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin
reserve n,a,b,c,d,e for Nat;
 c =b+3*a & e=a+b+c & d=3*e+b+c & a=6 & b=a+7 implies d=194;

これはノーエラーになります。どうですか? Mizar チェッカーは計算までして、結果が194であることを認めてくれました。

 でもMizarは194という計算結果までは教えてくれない、と言われるかもしれません。そこが電卓や計算用のプログラムと異なる所です。Mizarチェッカーは「合っている」あるいは「間違っている」というのみです。

 しかし考えてみるとこれは計算結果を教えるのと原理的には同じなのです。100以下か? と入れてエラーが出れば、100より大きい。200以下か?と入れてエラーが出なければ 100 < d <=200 ということが分かります。このようにしてだんだん範囲を狭めていけば194という値を知ることができるでしょう。

 例えて言うと自分では仕事をしないが、人の仕事が正しかったか正しくなかったかを冷静に判断できる人は仕事ができる人と同等の価値がある、ということです。