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

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

目次


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

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

第3節 条件分岐

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


テスト

Logをみる

Back
 

第6章 ソフトウェアの論理モデルT 第4節 プログラムの論理モデルと関数化

 上書きをしないプログラムを対応する論理式で置き換えたとき、その論理式をそのプログラムの「論理モデル logical model」ということにします。論理モデルでエラーが出なければそのプログラムは論理的には正しい、ということになります。

 ただし、数値がオーバーフローする可能性はあります。もっともMizarチェッカーの方も計算能力としてはあまり大きな数は扱えませんが。

 またプログラムの計算結果が出てもそれが適切なものであるかどうか、はプログラムの意味を考えなくてはいけません。例えば体脂肪率を求めるものであるとしたら、数式自体が医学的知識なくしては正しいかどうか決められないのです。

 しかし仕様 specification によって一度数学モデルが与えられると、そこから先は論理モデルが有効な世界になるのです。

 正しいプログラムは関数化することでそれを使って更に高度な正しいプログラムを作ることができます。

例1 次のプログラムは2つの非負の整数に対し差を与えるものであることを証明せよ。

 int diff_prg(int a,int b)
     {
      int d;
      if (a>=b){d=a-b;} else {d=b-a;}
      return d;
     }

解)このプログラムの論理モデルはMizarの関数の定義の形で与える。

reserve a,b for Integer;
definition let a,b;
func diff_prg(a,b) -> Integer means
:D00:  ((a>=b) implies it =a-b)&(not(a>=b)implies it=b-a);
existence;
uniqueness;
end;

そして次の定理においてそれが差を与えるものであることを証明する。

theorem a>=0 & b>=0 implies diff_prg(a,b)=max(a-b,b-a) & diff_prg(a,b)>=0;

差とは何か、という問題があり、定義D00 そのものである、ともいえるが、a-b と b-a の大きい方であり、それは非負のものである、ともいえる。実際それがそういう条件を与えていることを証明しているのが上の定理である。関数の定義は、その値が実際に存在することをexistenceの部分で示し、それが唯一であることをuniquenessの部分で示さなければいけない。

environ
  vocabulary ORDINAL2, ARYTM, ARYTM_1, ARYTM_3, ORDINAL1, NAT_1, XREAL_0,
    INT_1,SQUARE_1,DIFF_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS, XCMPLX_0,
    XREAL_0, REAL_1,NAT_1,INT_1,SQUARE_1;
 constructors REAL_1, XREAL_0, XCMPLX_0, XBOOLE_0,NAT_1,INT_1,SQUARE_1;
 clusters REAL_1, NUMBERS, ORDINAL2, XREAL_0, ARYTM_3, ZFMISC_1, XBOOLE_0,
      NAT_1,INT_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 theorems AXIOMS,SQUARE_1,REAL_2;
begin
reserve n,a,b,c,d,e for Integer;
definition let a,b;
func diff_prg(a,b) -> Integer means
:D00:  ((a>=b) implies it =a-b)&(not(a>=b)implies it=b-a);
existence
proof
  now per cases;
  case a>=b;
   hence ex i being Integer st
   ((a>=b) implies i =a-b)&(not(a>=b)implies i=b-a);
  end;
  case a=b) implies i =a-b)&(not(a>=b)implies i=b-a);
  end;
  end;
 hence ex i being Integer st
 ((a>=b) implies i =a-b)&(not(a>=b)implies i=b-a);
end;
uniqueness;
end;

theorem a>=0 & b>=0 implies diff_prg(a,b)=max(a-b,b-a) & diff_prg(a,b)>=0
proof assume a>=0 & b>=0;
  set i= diff_prg(a,b);
  now per cases;
  case B0: a>=b;then
    B1: i=a-b by D00;then
    B2: i>=0 by B0,SQUARE_1:12;
    b-a<=0 by B0,REAL_2:106;then
    b-a<=i by B2,AXIOMS:22;then
    max(a-b,b-a)=i by B1,SQUARE_1:def 2;
   hence diff_prg(a,b)=max(a-b,b-a) & diff_prg(a,b)>=0 by B1,B2;
  end;
  case B0: a=0 by B0,SQUARE_1:11;
    a-b<=0 by B0,REAL_2:106;then
    a-b<=i by B2,AXIOMS:22;then
    max(a-b,b-a)=i by B1,SQUARE_1:def 2;
   hence diff_prg(a,b)=max(a-b,b-a) & diff_prg(a,b)>=0 by B1,B2;
  end;
  end;
 hence thesis;
end;

定義において唯一性は特別証明しなくても正当である、とチェッカーが判断した。max の定義はSQUARE_1にある。また新しく次の内容のvocabularyファイル(DIFF_1.VOC)を与えている。

Odiff_prg

 上の定義は面白いものです。それはプログラムの関数化がうまくいっていることを証明するものであると同時に、Mizarでの関数のLibraryを与えるものでもあるからです。

 プログラムの関数即数学の関数でもあるのです。そしていずれにしても、プログラムの中でも、また数学の他の関数の定義の中でも使うことができる、という訳です。ソフトウェアの開発とは、数学の証明をすることである、ということがこれから徐々に一般にも認識されてくるでしょう。