sile/oosc-ch11-9-12.md

## oosc-ch11-9-12.md

      
    Raw
  

              oosc-ch11-9-12.md
            
          
    11.9 クラスが正しいのはいつか

11.9.1 クラスの正しさ


クラスが正しいかどうかは、クラス自身によるのではなく仕様に基づかなければならない
事前条件、事後条件、不変表明によってクラステキスト事態に、仕様のあたるものを入れ込むことが可能

定義: クラスの正しさ
クラスは、次の場合にのみ、その表明に関して正しい。

C1: 生成プロシージャpで、有効な引数の任意の集合x_pに対して、次の式が満たされている

{Default_c and pre_p(x_p)} Body_p {post_p(x_p) and ANV}


C2: 全てのエクスポートルーチンrと有効な引数の任意の集合に対して、次の式が満たされている

x_r{pre_r(x_r) and INV} Body_r {post_r(x_r) and INV}


図11.5を用いた補足説明

クラスに creation句 がないなら、デフォルト値が不変表明を満たす必要がある
顧客が事前条件を満たさずにルーチンを呼び出した場合は(契約が結べていないので）、ルーチンは何をしても良い(クラスの正しさ的には動作は未定義)

11.9.2 生成プロシージャの役割

生成されるクラスのインスタンスが不変表明を満たす状態になっていることを保証するのが役割
11.9.3 再び配列について

前章で扱ったライブラリクラスARRAYの定義に事前条件、事後条件、不変表明を追加。
11.10 ADTとの関係


クラスは抽象データ型(ADT)を実装したものの一つ
表明はADTの意味的な性質をクラスに再導入する一つの手段とみなすことができる

11.10.1 ただの関数の集合ではない

ADTは次の四つの要素からなる(復習):

型名。おそらく総称パラメータ付き (TYPESパラグラフ)
シグネチャ付き関数リスト (FUNCTIONSパラグラフ)
関数の結果の特性を示す公理 (AXIOMSパラグラフ)
関数の適用能力の制約 (PRECONDITIONSパラグラフ)

後者二つは重要:

見落とされることが多いが、この二つがなければADTの魅力は半減
事前条件と公理は関数の意味的特性を示す

これらが省略された場合でも情報隠蔽(カプセル化)は達成できるが、それだけ


OOPのもとに汎用的に作られたクラスのメソッド名は、具体的なものではなく一般的なものになりがちで名前からも意味が分かりにくい


ここで示された危険性は、オブジェクト指向ではプログラミングに波及する。つまり、対応する抽象データ型の操作を実装すると思われるルーチンは、原則的に、ほとんどどんな操作でもできてしまうが、表明を使うことで、意味的なものを取り戻し、この危険を避けることができる。

! ただし、主流なオブジェクト指向言語にはたいてい表明はない
11.10.2 クラス特性 vs. ADT関数

クラス特性と対応するADT(ADTの関数)との対応:

ADTには三種類(生成、問い合わせ、命令)の関数がある (詳細は6.4.4)
f: A x B x ... -> XのどこにADT(Tと表記)が出てくるかで関数のカテゴリが決まる

Tが矢印の右側にのみ現れる: ADTでは生成関数、対応するクラス特性は生成プロシージャ
Tが矢印の左側にのみ現れる: ADTでは問い合わせ関数、対応するクラス特性は属性もしくは関数
Tが矢印の両側に現れる: ADTでは命令関数、対応するクラス特性はオブジェクト更新プロシージャ(コマンドと呼ばれる)


11.10.3 公理の表現

意味的なADT特性とクラス表明との対応:

仕様の中の一つの関数に対する事前条件は、対応するルーチンの事前条件句として再現される
命令関数を含む公理は、対応するプロシージャの事後条件句として再現される
問い合わせ関数のみを含む公理は、対応する関数の事後条件句、もしくは不変表明句として再現される
構築関数を含む公理は、対応する生成プロシージャの事後条件に再現される

11.10.4 抽象化関数

図11.6は「C は A を正しく実装したものである」ということを示している
凡例:

A: 抽象データ型
C: ADTの実装クラス
af: ADT仕様の抽象関数
cf: クラスの具象特性
a↑: CのインスタンスからAのインスタンスへの抽象化関数 (たいてい部分関数であり　また 逆方向は関数ではないことが多い)

抽象データ型に適用可能なすべての関数afとそれらの実装cfに対して、次の式が成り立つならば、その実装は正しいといえる: (';'は関数間の結合演算子)

クラス-ADT整合性
(cf;a) = (a;af)

11.10.5 実装不変表明

不変表明に現れる表明で、ADTには直接対応するものがない表明が存在する

STACK4での例
実装不変表明(implementation invariant)として知られ、クラス不変表明の一種
対応するADTに対応する実装の中から、選択されたクラスの一貫性を表すのに役立つ

抽象化関数は一方向:

抽象オブジェクトに対応する具象オブジェクトの表現方法はいくつもあり得る
具象オブジェクトに対応する抽象オブジェクトは一つ

複数の抽象オブジェクトとから実装されると解釈できるならば、選ばれる表現はあいまいになり、ゆえに不適当


抽象化関数は(多くの場合は)部分関数:

全ての具象オブジェクトが抽象オブジェクトの有効な表現とは限らない

ex. スタックの実装オブジェクトで要素数が許容量を超えている場合


抽象化関数を適用できる(= 有効な具象オブジェクトであることを示す)ための表明が、実装不変表明
数学的な用語でいうと、実装不変表明は抽象化関数のドメインの特性関数

すなわち、その関数が適用可能であるときを定義する性質


実装不変表明はクラス表明の一種である。ただし、抽象データ型仕様に対応するものは存在しない。つまり、抽象データ型には関係せず、表現にだけ関係するもので、具象オブジェクト候補が、確かにただ1つの抽象オブジェクトから実装されたものである場合を定義している。

11.11 表明命令

check命令の話

C言語のassertに近い

関数の入口以外で、特定の性質が満たされていなければならないことを(ソフトウェアを書く人に)表現する手段。
エラー処理がないのは書き忘れ(バグ)ではなく、意図的なもの(ex. その前段の処理によって正しいことが保障されている)であることを示す場合にも有用。
開発に実装者が仮定していた性質を、具体的なソフトウェアテキストとして残しておくことができる。
(後日の変更時に悩まなくて済む)
check命令を本当時に実行可能な命令に切り替えることもできます。
11.12 ループ不変表明と変化表明

オブジェクト指向とは独立したものだが、これまでのメカニズムを上手に補足してくれるものなので取りあげる。
11.12.1 ループの問題

ループは重要。
問題も起きやすい。

1つ違い(off-by-one)
空の構造といった境界にあたるケースの取り扱いが不適切
無限ループ

! 最近よくあるforeach構文やforeach関数(or 関数型言語的なデータに対する関数群の連鎖的な適用)は、これらの問題の一部を解消する(ように思う)
図11.8 二分探索での例

アイディアが簡単なのに、実装が大変(間違いが混入しやすい)
「結局、それぞれのアルゴリズムに対して、適切に動かないケースを見つけるために、自分で検査しなければならない破目に陥る」

11.12.2 ループを正しくする


表明を賢く使えば、先のような問題を避けることができる
ループ不変表明 and/or (表明ではなく整数式である)ループ変化表明、を使えばループが正しいことが保障される

ループとは 逐次近似(successive approximation) によって特定の結果を算出する方法の1つである。

配列中の最大値を求める例
Resultの初期値を先頭要素にした後に、徐々にスライスして対象範囲を広げていく
この例における不変表明で示される性質は「ループの各段階で、Resultが、現時点での配列の近似における最大値を持つ」というもの

最終的にスライスが配列全体をカバーした段階で、不変表明が各段階で守られていることにより、最大値が適切に求められたことが分かる


11.12.3 正しいと思われるループの成分

配列の例で用いた仕組みの一般化。
図11.10 ループの計算
ループの計算の成分:

目的post: 事後条件。ループによって得られる(期待通りの)結果。 (図: 集合POST)
不変表明の特性inv: 目的とするものを一般化したもの。目的とするものは、その中の特殊ケースの一つ。(図: 集合INV)
最初の時点init: INV内に存在する処理の開始地点
変換body: INVの中には入っているが、POSTには入っていない点から出発し、INVの中にあり、しかもPOSTに近づく点を作成する
変化表明: bodyを多数適用した中で上限値、INVの中にあって、POSTに到達するのに必要となるもの (詳しくは後述)

変化表明の役割:

純粋な数学と違い、プログラムでは逐次近似のすべてにおいて、有限回の繰り返しで目的に到達しなければならない
ループのプロセスが終了することを保証する具体的な方法は、ループとある整数値を関係付けること
この整数値がループ変化表明

変化表明の性質:

変化表明は決して負にはなってはいけない
ループ本体を実行するごとに変化表明は減少する

これらの性質が守られていれば、ループが有限回で終わることが保障される


配列の最大値の例のような単純なループなら終了判定は簡単。
もっと複雑なループでは、繰り返しの回数は、前もって計算できるほど簡単ではない。

終了することを確かめるのは大いなる挑戦
唯一の一般解が変化表明を見つけること

繰り返しが目的(事後条件)に達したかどうかを簡単に判定する方法も必要。
11.12.4 ループの構文

11.12.3を踏まえたループ構文の話。
ループ構文に必要な要素:

ループ不変表明inv (表明)
終了条件exit。invとの論理積で、期待される目的に到達する
変化表明var (整数式)
初期化命令の集合init。必ずinvを満たす状態を生じ、varを負でない値にする
本体命令の集合body

invが成立し、varが負でない状態で始まり、
不変表明を保持し、
変化表明が負でない間は、それを減少させる


from
    init
invariant -- optional
    inv
variant -- optional
    var
until
    exit
loop
    body
end
配列の最大値を求める例:
from
    i := t.lower; Result := t @ lower
invariant
    -- Resultは、t.lowerからiまでのインデックスで、tの要素が最大となる値である
variant
    t.lower - i
until
    i = t.upper
loop
    i := i + 1
    Result := Result.max (t @ i)
end
※ 不変表明がコメントによってなされている件に関しては「11.14.2節 表明の記述能力」を参照
最大公約数(gcd)をユークリッドのアルゴリズムを使って計算する例:
gcd (a, b: INTEGER): INTEGER is
        -- a と b の最大公約数
    require
        a > 0; b > 0
    local
        x, y: INTEGER
    do
        from
            x := a; y := b
        invariant
            x > 0; y > 0
            -- <x,y>のペアは<a,b>のペアと同じ最大公約数を持つ
        variant
            x.max (y)
        until
            x = y
        loop
            if x > y then x := x - y else y := y - x end
        end
        Result := x
    ensure
        -- Resultにはaとbの最大公約数が入っている
end

前にもいったように、invariant句とvariant句は指定しなくてもよい。しかし、この句があれば、ループの目的は明確になり、正しさをチェックすることができる。また、そこそこのループであれば、興味深い不変表明と変化表明によって、その特徴を表すことができる。したがって、不変表明と変化表明を含む、これ以降の章で扱うたくさんの例によって、その基幹アルゴリズムや正しさを掘り下げることができる。