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

 第3節 条件分岐

目次


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

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

第3節 条件分岐

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


テスト

Logをみる

Back
 

第6章 ソフトウェアの論理モデルT  第3節 条件分岐

 前節では、直列的に代入を伴った計算をするプログラム(上書きをしない non-overwriting)の正しさ、について説明しました。

 条件分岐が入るとどうでしょうか?

例1 次のプログラムで d の値はどうなるか?

     int a,b,c,d;
     a=7;
     b=a+9;
     c=a*3+5*b+6;
     if(c < 80){d=a+b+c;} else {if(c < 100){d=a+2*b+c;} else {d=a+3*b+c;}}

解)まず b の値を求めると

  b=a+9=16

次に c の値を求めると

  c = 7*3+5*16+6=21+80+6=107

条件分岐では最後のelseの場合であるから

    d = 7+3*16+107=7+48+107=162

が答えである。

上のプログラムは上書きをしていません。条件分岐をしたどのケースでもそうです。したがってプログラムは次の命題論理式と同等です。

 reserve a,b,c,d for Nat;
  a=7 & b=a+9 & c =a*3+5*b+6 &
  (c <80 implies d=a+b+c)&
  (not c <80 implies ( c <100 implies d=a+2*b+c)&
                     ((not c <100) implies d=a+3*b+c))
  implies d=162;

これをチェックしてエラーが出なければ確かにこのプログラムはd=162 を結果として与えることになります。なお c= は集合の包含関係の記号として予約されていますので間にスペースを入れて c =とします。c< は真部分集合の記号として予約されていますのでやはり間にスペースを入れます。

 実際に前節と同じ環境部のもとでチェックしますとエラーは0です。

 if 文は A implies B; という形式の文に変えます。else がついている場合には

 (A implies B)&(not A implies C)

という形の文に変えます。if 文が何重にもなっている場合は結論式のところにまた該当するimplies文を入れればいいのです。

 なお変数が負の値をとる可能性があるときは変数の型を Integer とします。このときは環境部にINT_1 を加えます。a=-1 としたときの例を示します。

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

begin
reserve n,a,b,c,d,e for Integer;
   a= -1 & b=a+9 & c =a*3+5*b+6 &
   (c <80 implies d=a+b+c)&
   (not c <80 implies ( c <100 implies d=a+2*b+c)&
                      ((not c <100) implies d=a+3*b+c))
    implies d=50;