AN INVITATION TO EIFFEL

5 表明

　クラスは、もしその定義を抽象データ型の実装として値するならば、利用可能な操作からだけではなく、その操作の形式的特性からも、知られていなければなりません。これは、今まで述べた例にはありません。

5.1 表明の役割

　Eiffel は、ソフトウェア開発者に、表明<assertion>を書くことによってクラスの形式的特性を表現することを促します。表明は、とりわけ、次の役割において現れることがあります。

ルーチンの 事前条件<precondition>は、クライアントがルーチンを呼び出すときにいつも満足しなければならない要件を表現します。たとえば、 ACCOUNT の設計者は、口座<account>の残高<balance>を最小値以上に保っているときにだけ引き出し<withdrawal>の操作を許したいと願っているかもしれません。事前条件は、require というキーワードによって導入します。

ルーチンの 事後条件<postcondition>は、ensure というキーワードによって導入し、ルーチン（供給者<supplier>）が復帰時に保証する条件を表します。ただし、事前条件が入り口で満足されていた場合に限ります。

クラスの不変条件<invariants>は、実例が外部からアクセス可能であるときはいつでも、つまり、そのクラスの公開<expose>されたルーチンへのどんな呼出しの後でも、そのクラスのあらゆる実例によって満足させられなければなりません。不変条件は、invariant というキーワードによって導入される句に現われ、そのクラスのすべてのルーチンに取り込まれる<inpose>、一般的で首尾一貫した制約を表します。

　ふさわしい表明を用いると、ACCOUNT クラスは、次のようになります。

class ACCOUNT creation

make


feature


... 既出の通りの属性: balance, minimum_balance, owner, open ...



deposit (sum: INTEGER) is

-- 口座へ sum を預け入れる

require

sum >= 0

do

add (sum)

ensure

balance = old balance + sum

end;


withdraw (sum: INTEGER) is

-- 口座から sum を引き出す

require

sum >= 0

sum <= balance - minimum_balance

do

add (-sum)

ensure

balance = old balance - sum

end;



may_withdraw ... -- 既出の通り



feature {NONE}



add ... -- 前の通り



make (initial: INTEGER) is

-- 初期値 initial で口座を初期化する

require

initial >= minimum_balance

do

balance := initial

end

invariant



balance >= minimum_balance

end -- class ACCOUNT

　old attribute_name という表記法は、ルーチンの事後条件においてだけ使用してもかまいません。それは、その属性がルーチンの入り口で得た値を明示します。

5.2 生成手続き

　上記の最終版で、今度は、クラスは、生成<creation>手続き make を含んでいます。ACCOUNT の最初のバージョンで、クライアントは、口座を生成するために、!! acc1 といった生成命令を使用していましたが、それはデフォルトの初期化であり、口座にゼロを設定し、不変条件を脅かすものでした。クラス テキストの始まりにあるcreation句に並べた、一つ以上の生成手続きを持つことによって、クラスは、デフォルトの初期化を再定義<override>する方法を提供します。次の例の効果は、

!! acc1.make (5_500)

オブジェクトを割り付けることと、所与の引数を伴って、このオブジェクト上の手続き make を呼び出すことです。この呼出しが正しいのは、事前条件を満足させるからであり、不変条件を保証することになります（整数定数の 5_500 における下線文字 "_" は、意味のある効果をもちません。一般規則は、あなたは、整数定数の可読性を向上させるために、右から三桁ずつ数字をグループ化できる、ということです）。

　さもなくば、make のような、creation 句に並べられた手続きは、他のルーチンと同じ特性、特に呼出しのために活躍します。ここで、手続き make が非公開<secret>であるのは、feature {NONE} で始まる句に現れているからです。それため、クライアントが次のような呼出しを含むことは無効になります。

acc.make (8_000)

　このような呼出しを有効にするためには、make の宣言をクラス ACCOUNT の最初の feature 句へ移動すれば十分でしょう。この並びは、公開の制限を何一つ課しません。このような呼出しは、新たなオブジェクトを何も生成しませんが、単に、直前で生成された口座の残高をリセットします。

5.3 契約による設計

　文法的に、表明は、old 表記法のような、わずかな拡張を持った、真理値式です。セミコロン（ withdraw への事前条件を見てください）は、"and" と等価ですが、構成部品<component>の個々の識別を認めます。

　表明は、信頼性の高い、オブジェクト指向によるソフトウェアを構築するために、Eiffel 手法における中心的な部分を演じます。表明は、プログラマがソフトウェアの要素を書くときに正しいと信じて頼っている仮定を明示させる働きがあります。表明、特に事前条件と事後条件、を書くことは、ルーチンとその呼出し元との関係を支配する 契約<contract> の点から、略さずに書くことに相当します。事前条件は呼出し元を束縛し、事後条件はそのルーチンを束縛します。

　Eiffel 手法の中心部分である 契約による設計 の基にある理論は、ソフトウェア構築を、共通の義務と表明によって明示させられた利益とに頼っている、クライアント（呼出し元）とサプライヤ（ルーチン）間の契約に基づくものとして捉えます。

5.4 簡潔な書式

　表明は、再利用可能なソフトウェア コンポーネントの文書化のための不可欠なツールでもあります。あらゆるオブジェクトが何を期待し（事前条件）、復帰するときに何を保証し（事後条件）、どんな普遍的な条件を維持するか（不変条件）、ということについての正確な文書無しでは、大規模な再利用を期待できません。

　EiffelBenchの文書化ツールは、表明を、実装ではなく観察可能な振る舞いの点からクラスを説明する、クライアントのプログラマのための情報をプロデュースするために使用します。特に、クラスのインターフェイスの文書として働く、クラスの簡潔な書式は、完全なテキストから、すべての非公開の特徴と、ルーチンのdo句のようなすべての実装上の情報とを取り除き、インターフェイスの情報と特に表明とを保持することによって獲得できます。

class interface ACCOUNT creation


make


feature


balance: INTEGER;

...


deposit (sum: INTEGER) is

-- Deposit sum into the account.

require

sum >= 0

ensure

balance = old balance + sum



withdraw (sum: INTEGER) is

-- Withdraw sum from the account.

require

sum >= 0;

sum <= balance - minimum_balance

ensure

balance = old balance - sum

may_withdraw ...

end -- class ACCOUNT

　これは、実際の Eiffel ではなく、Eiffel クラスの単なる文書であり、それゆえ、混乱を避けるために、わずかに異なる構文を使用しています（クラスというよりはむしろクラスのインターフェイスです）。上で行った観察に従って、 balance のための出力は、もしこの特徴が属性というよりも関数であったならば、同じであったでしょう。

　ISE Eiffel の環境では、簡潔な書式は、An Object-Oriented Environment: Principles and Application という本で説明されている自動的なツール群によって作成されます。あなたは、``Guided Tour'' of EiffelBench というオンライン上のウェッブでそれらに対する流行のものを取得できます（EiffelBench の Class Tool のmention of the Short button を見てください。discussion of browsing facilitiesの一部にもなっています）。それは、クラスの文書化の主要な書式として働きます。変種である、平易で簡潔な書式は、クラス自体で導入された特徴とは別に、継承した特徴を含むことによって、account への継承を取ります。

　実行時に表明を評価することも可能なので、潜在的なエラー（"bugs"）を網羅しないようにもできます。実装は、表明の監視について、事前条件だけとか事後条件だけとかなどといった、いくつかの水準を提供します。監視がオンであるとき、真へ評価する表明は、実行へは何の影響も与えません。偽へ評価する表明は、次に説明するような、例外を誘発するでしょう。つまり、ソフトウェア開発者が適した例外処理を書いている限り、例外は、正確なエラーメッセージと呼び出し追跡<call trace>を伴ったエラーメッセージと停止を引き起こすでしょう。

　この表明を検査する能力は、強力なテストとデバッグの機構を提供します。特に、Eiffel のソフトウェア開発で広範囲に使用されている EiffelBase ライブラリのクラス群が、注意深く書かれた表明によって保護されているからです。

　しかしながら、実行時検査は、表明の一つのアプリケーションに限られます。設計と文書化の特効薬としての役割は、契約による設計の理論の一部分として、ソフトウェア開発の Eiffel の様式に広がる影響を及ぼします。