Software Engineering Lecture s2

Menu Menu

先週の復習

論理式の意味

論理式は、個々の構文要素に意味を対応する。ここでは、M(Q)という関数で論理式の意味を定義する。意味(Meaning)は、数学的な集合で、前もって定義されているとする。

Mの()の中に来るのは「記号列としての論理式」であって、 

    P
    Q
    P ∨ Q
    P ∧ Q
    ¬P
    ( P ∧ Q ) ∧ Q
とかが来る。この部分は、例えば、Java では、木構造を使って実現することができる。∧ とかの演算子であること、あるいは、PとかQ が変数を表すこと、() を使って、演算子のネスト(入れ子)を制御できることなどは、通常のプログラム言語に似ている。それに関して、細かく定義することは、自明なのでここではしない。

命題論理の場合は、M(Q) の値は、{T,F} の集合の要素、つまり、真か偽のどちらかである。例えば、PとかQ の変数の値は、前もって、T か F に決める。その決め方に従って、 

    M(Q) = T
    M(P) = F
ということになる。「変数Q の意味(値)は、Tである」というように読む。

より複雑な論理式に対しては、M(Q) は、以下のように、記号列の構造(木構造)にそって決める。

M(P ∨ Q) = M (P) ∨ M (Q)
M(P ∧ Q) = M (P) ∧ M (Q)
M(¬P) = ¬ M(P)

右側の論理記号は既に知られている。(これで定義したことになるのか?)命題論理の場合は、これらは真理値表で定義することが出来る。

M(P) M(Q) M(P)∧ M(P) M(P)∨ M(Q) ¬ M(P)
T T TT F
T F FT F
F T FT T
F F FF T

この定義を使って命題論理式の値を計算することができる。

命題変数は、変数と真偽値を対応させる関数を定義する。
M(P) = T または F
これは変数の値の割当てである。変数は、変数に対応する集合の値、述語や関数は、それぞれに対応する写像に対応づけられる。

この対応を変更することにより論理式の真偽が変わる。変数の対応を論理式のインタープリテーション(Interpretation)という。

与えられた論理式を真にするようなインタープリテーションを論理式のモデル(Model)という。

Java で命題論理を記述する

問題2.1

命題変数A,B の A=T, B=F として、次の論理式の値を計算せよ。

1. A∧ ¬B
2. ¬A∨¬B
3. (¬A∨¬B)∧(A∧ ¬B )
4. (¬A∨B)∨¬(A∧ B )
5. (A∧¬B)∧(A∧B )

A,B の値を入力として、これらの論理式の値を計算するプログラムをJava で作成せよ。

与えられた論理式が、
恒真 Valid すべてのインタプリテーションに対して論理式が真
充足可能 Statisfiable あるインタプリテーションに対して論理式が真
充足不可能 Unsatisfaible どんなインタプリテーションに対しても論理式が真にならない
かどうかを調べるプログラムを Java で作成せよ。

A,B の値すべての組合せを試して、与えられた論理式のモデルを求める(あるとは限らない) を与えるJava のプログラムを作成せよ。

作成したプログラムの計算量について考察せよ。

論理とプログラムの対応

プログラムには変数と関数(サブルーチン)が存在する。これに対応する論理は、一階述語述語論理と呼ばれる。述語論理は、変数や関数の値の集合V に対して、以下のように定義される

M(v) (定数)= v ∈ V
M(x) (変数)= x に対して決まった v ∈ V
M(f(x0,x1,...xn) (関数)= V x ... x V → V
M(p(x0,x1,...xn) (述語)=> V x ... x V → {T,F}
M(P ∧ Q) = M (P) ∧ M (Q)
M(¬P) = ¬ M(P)
M(∃(x)(p(x)))= ある v ∈ V に対して M(p(v))
M(∀(x)(p(x)))= すべて v ∈ V に対して M(p(v))

V x V は集合の直積。前回習ったように、関数は集合の直積の部分集合で表される。要素の組を作るのが直積。部分集合の集合は集合の巾ともいう。V → V は、Vの巾集合の要素である。

f(x) は {(input1,output1),(input2,output2),...,(inputn,outputn)}
変数と値と対応、関数と部分集合の対応、述語の真偽値への対応が、述語論理式のインタープリテーションとなる。(変数に関数や述語を許すと二階述語論理となる)

述語論理式の値を計算するプログラムはインタプリタになる。

整数論を含む述語論理式の恒真性を調べるプログラムは存在しないことが知られている。(一階述語論理の決定不能性) これは、プログラムの停止性の決定不能性に対応している。

仕様は、一階述語論理で記述され、プログラム(に対応する一階述語論理式) がそれを満たしているかどうかを調べることは、以下の論理式の性質を調べることになる。仕様S, プログラムを表す論理式Pに対して、 

	P → S
M(P) M(Q) M(P)→M(P)
T T T
T F F
F T T
F F T

プログラムには入力(I)と出力(O)があるので、

P(I1,I2,...In,O1,O2,...On )
→
S(I1,I2,...In,O1,O2,...On)

となる。この論理式が、
恒真 正しいプログラム
否定が充足可能 プログラムにバグがある
ということになる。

述語論理に基づいたプログラミング言語としては、Prolog というのがある。集合に基づいた仕様記述言語としては、Z言語というのがある。

問題2.2

入力と出力がすべての述語と関数について有限ならば論理式の恒真性はチェックできる。 

    ∀x>1 (x^2 > x)
をx∈{2,3,4,5,6}について調べよ。また、これを調べるJavaのプログラムを記述せよ。

動けば良いだけのプログラミングから、良いプログラムへ

動かせるだけが精一杯、人のプログラムをコピーして手直し。それでいいのか?

例えば、「プログラム書法第二版」Brian W.Kernighan ISBN4-320-02085-5 C3041 は、Fortan を使ったすごく古い本だが、今でも有効な規則が多く載っている。

最近だと、「プログラム作法」というのが良い本だと思われる。

もし、もう少し、チームプログラミングや、深い知識を得たいのならば、「コード・コンプリート」という本が良い。

  • ライブラリ関数を使おう
  • 効率のために、わかりやすさを犠牲にしてはいけない
  • 多方向の枝分かれをつくる時には if..else if. else を使おう
  • プログラムが簡単になるようなデータの表現を選ぼう
  • 第一版ができたところでやめてしまってはいけない。
  • だめなプログラムを修正するのはやめて、全部書き直そう
  • 大きいプログラムは小部分ごとに書き、テストするようにしよう
  • 入力の妥当性、現実性をテストしよう
  • 読み合わせのしやすい入力形式を選ぼう
  • 入出力はサブルーチンの中に閉じ込めよう
  • すべての変数を使う前に忘れずに初期化しよう (-Wall -O)
  • 虫取り向きのコンパイラを使おう
  • プログラムを境界値でテストしよう
  • 0.1の10.0倍は1.0にはならない
  • 速くする前に正しくしよう
  • 速くしたかったら単純さを保とう
  • プログラムをひねくりまわすのはやめて、もっと良いアルゴリズムをみつけよう
  • 注釈とプログラムを一致させよう
  • 意味のある変数名を使おう

    もちろん、今となっては、まちがっている規則もたくさんある。「一時変数はなるべく使わない」なんていう規則はもはや時代遅れだといえる。

    良いプログラムとは何か?

    どんなにきれいに書いてあり、どんなに規則に従っていても、間違ったプログラムは、良いプログラムとはいえない。

    良いプログラムを読む

    プログラムはどこにあるの?

    正しいプログラムかどうかを調べる

    仕様は論理式により記述し、プログラムはそれを関数を使って実現する。ただし、現在のプログラムには変数の値が変わるという現象があるので、単純な一階述語論理にならない。

    変数の値を変えないという方針をとると一階述語論理に近くなる。一旦代入した変数の値を変えないとプログラムの見通しが良くなる場合がある。(単一代入)

    プログラムが正しく仕様を満たしているかどうかを調べる方法はいろいろある。一つは、プログラムのステートメントごとに、その前後で満たしている性質を論理式で記述する方法である。これはHoare logic と呼ばれる。 

        {Pre Condition}
        S
    {Post Condition}
    例えば、 

        {b!=0 ∧ gcd(a,b) = gcd(x,y)}
        a := a mod b
    {gcd(a,b) = gcd(x,y)}
    この場合は、gcd(a,b)=gcd(x,y) というのがstatement a:= a mod b の前後で保存されている。このようなものを、不変式という。

    Pre Condition は、Post Condition から計算することができる。例えば、 

        { 0<i ∧  i<100 }
    というPost Condition があった時に、 
        i := i+1
    というステートメントのPre Condition は、 
        { 0<i-1 ∧  i-1<100 }
    となる。

    ループ(while文、for文)などがある場合は、Post Condition と Pre Condition が不変式となるようなものを発見すればPost Condition から Pre Condition を見付けることができる。

    必要な出力に対する Post Condition から、入力に対するPre Condition を見つけ出せると、正しい出力を得るための入力条件を見付けられたことになる。

    ただし、Pre Condition はループが終了することを保証しない。それは、また、別途、証明する必要がある。

    証明、健全性、完全性

    このようにプログラムが正しく動作することは、論理式の変形として理解することができる。プログラムが正しく動作することと、それを証明できることには以下のような関係がある。

    健全性: 

    	証明されたプログラムは、正しく動作する
    完全性: 
    	正しく動作するプログラムには、必ず証明がある
    実際にはループの間で、どのような不変式が成り立つかを見付けることが、Hoare logic によるプログラムの検証の重要な部分になる。これを使って理論的にはほとんどのプログラムを正しさを証明することができるはずである。でも、実際にやってみると、などの問題があって、実用的でない。だからといって勉強しなくても良いわけではない。(参考文献: プログラム検証論 林 晋 共立出版 ISBN4-320-02658-6) </p>

    さらに、正しく動作するかどうか決定できないプログラムがある言うことががゲーデルによって示されている。なので、プログラム検証には本質的な限界がある。

    自動証明

    証明は基本的には記号的な操作だが、コンピュータプログラムに対しては極めて長くなることが多い。(60-300page など)

    だとすれば、証明自体をコンピュータにやらせるのが良いだろう。

    HOL Theorem prover Reference site for HOL

    Object 指向と論理

    Object 指向言語は、関数呼び出しの先頭に self を表す構造体が付いているのと本質的には変わりがない。なので、Object 指向言語も同様に、正しさを証明することが出来る。

    しかし、一方で、Object の中に閉じたプログラムの正しさを証明する必要がある。例えば、継承とか移譲とかが、証明の中でどういう性質を持つのかを考察するのは難しい。

    問題2.3

    HOL (Hihger Order Logic ) に関して、調べてみよう。

    HOLのinstallの仕方 HOLのTutorial

    • Shinji KONO / Tue May 13 11:33:21 2008