Eiffel に入門した
モチベーション
- 「Good Code, Bad Code」読んでて Eiffel という言語があるだなってことを知った
- Eiffelは、契約による設計を中心に作られたオブジェクト指向プログラミング言語ってのを知ってなんかよく聞くような話だなと思い興味をもった
先に参考にしたドキュメントを載せておく。
- https://www.eiffel.org/doc/eiffel/Your_next_project_in_Eiffel
- https://eiffel-guide.com/
- https://en.wikipedia.org/wiki/Eiffel_(programming_language)
Eiffelの特徴
契約による設計
Eiffelは、仕様をコードに直接組み込む「契約」によって、プログラムの正当性を保証する。
-
事前条件 (
require)- ルーチンが呼び出される前に満たすべき条件
-
事後条件 (
ensure)- ルーチン実行後に保証されるべき条件
-
不変条件 (
invariant)- クラス全体を通じて常に維持される条件
class
BANK_ACCOUNT
feature
balance: INTEGER -- 口座の残高
deposit (amount: INTEGER)
require
amount > 0 -- 預ける金額は正の値
do
balance := balance + amount
ensure
balance = old balance + amount -- 残高が正しく増加している
end
invariant
balance >= 0 -- 残高は常に0以上
end
マルチ継承
複数の親クラスを継承できる。
個人的に継承はコードを追いづらくなるイメージが強くあまり好きになれていない。
強力な型安全性
ジェネリクスも使える。モダンだね。
セットアップ & 基本形をみる
EiffelStudio というのがあるが、セットアップするのめんどくさい。
たいていオンラインエディターあるよねってことで、https:--codeboard.eiffel.org/ をみつけた。
Language セレクトボックス、一個しか選択肢ないのカワイイ
基本形は次のようになる。
公式がちょっとわかりにくかったので https:--eiffel-guide.com/ を読みながら。
class -- クラス定義
APPLICATION
create -- コンストラクタの宣言（コンストラクタが必要ない場合は省略可）
make
feature -- クラスのプロパティやメソッド。do で始まり、end で終える
make
do
print ("Hello Eiffel World!%N")
end
end
コンパイルして実行すると Hello Eiffel World! が出力された。
application.e というファイルだがここをエントリポイントとしている。
アプリケーションを作る
じゃあちょっとアプリを作ってみる。
カウンターアプリにして、契約と不変条件を活用できるようにする。
カウンタークラス
- 指定された範囲（
min_valueからmax_value）内でカウント値を増減するクラスである
## ルーチン
- `make`
- 責務
- カウンターを初期化する
- 事前条件 (`require`)
- 最小値が最大値を超えていないこと
- 処理内容
- `min_value` に `a_min_value` を設定
- `max_value` に `a_max_value` を設定
- `value` に `min_value` を設定
- 事後条件 (`ensure`)
- 最小値が正しく設定されている
- 最大値が正しく設定されている
- カウント値が初期化されている
- `increment`
- 責務
- カウンターの値を1増加する
- 事前条件 (`require`)
- 現在の値が最大値未満であること
- 処理内容
- `value` を1増加させる
- 事後条件 (`ensure`)
- 値が正しく1増加している
- `decrement`
- 責務
- カウンターの値を1減少する
- 事前条件 (`require`)
- 現在の値が最小値より大きいこと
- 処理内容
- `value` を1減少させる
- 事後条件 (`ensure`)
- 値が正しく1減少している
## 不変条件（`invariant`)
- クラスの全期間において以下の条件を保証する。
- カウント値は常に下限値以上
- カウント値は常に上限値以下
仕様を反映したコードは以下。
class
COUNTER
create
make
feature
value: INTEGER -- 現在のカウント値
max_value: INTEGER -- カウンターの最大値
min_value: INTEGER -- カウンターの最小値
-- カウンターを初期化
make (a_min_value: INTEGER; a_max_value: INTEGER)
require
a_min_value <= a_max_value
do
min_value := a_min_value
max_value := a_max_value
value := a_min_value
ensure
min_value = a_min_value
max_value = a_max_value
value = min_value
end
-- カウントを1増加
increment
require
value < max_value
do
value := value + 1
ensure
value = old value + 1
end
-- カウントを1減少
decrement
require
value > min_value
do
value := value - 1
ensure
value = old value - 1
end
-- 不変条件
invariant
value >= min_value and value <= max_value
end
アプリケーションクラス
エントリポイントとして COUNTER クラスを呼び、実行する。
class
APPLICATION
create
make
feature
make
-- counter class を make のローカル変数として定義
local
counter: COUNTER
do
-- カウンターを0から10の範囲で初期化
create counter.make(0, 10)
print ("初期値は..." + counter.value.out + "%N")
-- 増加
counter.increment
print ("+1すると..." + counter.value.out + "%N")
-- 減少
counter.decrement
print ("-1すると..." + counter.value.out + "%N")
end
end
実行結果してみる
ここでそれぞれの契約が効いていることも確認できる。
たとえば、 counter.make(10, 0) とすると make の事前条件に引っかかり、例外となる。↓
最小値が0だが、-1 になるようにしてみる。↓
２回目の decrement 時に事前条件の制約に引っかかりプログラムがきちんと落ちることを確認できる。
あと ensure のところにある old ってのも面白い。
ルーチンの実行前の状態を参照するみたい。
increment
ensure
value = old value + 1
- 右辺の
old value→ ルーチン実行前のvalue - 左辺の
value→ ルーチン実行後のvalue
ルーチン実行後の値は前の値に +1 したものになるよねというのを事後条件で保証している。
C#との違い
せっかくなので自分が普段使っている C# と比べてみる。
Effiel は言語仕様として契約による設計を組み込んでいるが C# はそんな感じではないよなぁ。
アプリケーション側でモデリングしてエラーやカスタム例外などでハンドリングするイメージがある。
継承もマルチ継承ではない。C# はインターフェースだと多重継承できるはず。
型はどっちも強く付いていいね。
余談(memo)
.NET Framework までは Code Contracts ってのがあったみたい。
↑ ちゃんと読んでないけど「あんまり使われないよね。いらねーよ」って感じでなくなったのかな？
結び
Eiffel は要求の文書化、検証をその通りやってくれるなぁと感じた。
require、ensure、invariant で契約がそのまま要求仕様としてそのまま機能し、ランタイムで契約の違反を確認できると。
なので適切に扱うことができれば仕様と実装が乖離しなくて済みそうだと思ったり。
そいういえば、.NET には HttpResponseMessage の EnsureSuccessStatusCode というものがある。
実行後に「レスポンスが成功である」という状態を保証し、それ以外の場合は例外をスローするというのである意味、事後条件を担っている。
達人プログラマーに一年に一つは新しい言語を学習しろってあったけど、僕はこの時点ですでに新しい言語を学習した。
また来年。
Discussion