情報証明論 第8章 プログラムの関数化

第3節 引数への結果代入

目次


第1節 配列と関数の値

第2節 関数が関数を呼ぶ

第3節 引数への結果代入


テスト

Logをみる

Back
 

第8章 プログラムの関数化 第3節 引数への結果代入

 関数プログラムを利用する場合、関数の値だけが戻り値であるわけでなく、引数の変数に結果が代入される場合もあります。

 例えば結果が配列であるようなとき、実際の値を引き渡すにはたくさんの値のコピーをしなければならず、時間が無駄になります。

 ポインタ値だけ引き渡す、ということも考えられますが、関数の中で関数を使うようなことを何重にも行った場合、込み入ってきて訳がわからなくなります。

 引数に計算結果を入れたいようなときは、その論理モデルは述語命題の形になります。そしてその正しさは定義に引き続く定理で与えます。

 特にそういう引数が存在すること、そしてその引数は求める条件を満たすこと、を証明します。ここでの議論は主に論文ファイル PRGCOR_2 によるものです。

例1 次の関数プログラムの論理モデルを示し、それがベクトルの和を与えるものであることを示す定理を示せ。証明は必要ない。

 void addvect_prg(float c[MAX_N],float a[MAX_N],float b[MAX_N])
 { int i;
   for (i=1;i<=MAX_N;i++)
   {
     c[i]=a[i]+b[i];
   }
 }

解)この論理モデルは

definition let c,a,b be FinSequence of REAL;
pred addvect_prg c,a,b means
 :AA: len c =MAX_N & len a=MAX_N & len b=MAX_N & 
  for i being Nat st 1<=i & i<=MAX_N holds 
    c/.i =a/.i +b/.i;
end;

で与えられる述語命題addvect_prgであり、正しさを示す定理は

theorem BB: for a,b being FinSequence of REAL holds 
(ex c being FinSequence of REAL
 st addvect_prg c,a,b);

theorem CC: for c,a,b being FinSequence of REAL st 
 addvect_prg c,a,b holds c =a+b;

である。ここで定理CCにあるa+bという演算は実ベクトルの和で、RVSUM_1:def 4で与えられるものである。