科学的モデルの作成と検討～『共変化』モデルと『タイプ置換原理』

自社の『科学的モデリングツール】によるタイプ整合性の自動検証とコードの完全自動生成～状変化モデル

継承の種類と推論条件を変更するとツールがタイプ置換原理によるスーパータイプとサブタイプの動作の整合性を自動判する。

幾つかの色で判定結果を表示する。

このツールではモデルで継承されたサブクラスで型の「共変化」の対応が出来るようにしている。

「共変化」はEiffelで取り入れられている重要なモデリングおよび実装の型の考え方である。
JavaやC++では「共変化」を認めていない「無変化」言語である。
(正確に言うとC+＋は返値の型に「共変化」を認めている。)

ただし、「共変化」を認めるEiffelが優れていて、C++やJavaが劣っている訳ではない。
「共変化」を認めるか認めないかは言語上の選択であり、短所・長所がどちらにもあるからだ。

それでも、サブタイプ(サブクラス)で「共変化」を認めないと実システムのモデリングになかりの
制約を与える事になる。

例えば、ガンマ達のデザインパターンの多くは「共変化のモデル」のパターンである。
つまり、リスコフ置換原理などのタイプ置換原理をある一定の条件下の元で満たさないことを認めているモデルであるのでプログラマーが事前条件や事後条件でしっかりチェックしないといけない。

この自社のツールではJavaやC++では共変化を認めていないので、サブクラスが継承した関数の事前条件で動的型チェックを行っている。
動的型チェックで不正な型のインスタンスの代入を防ぐことになる。
このようなアプローチが非常に重要である。

なお、Eiffelは高度な型推論を使いコンパイラーが動的に判定しcatコールを防いでいる。Eiffelではプログラマーにキャストする方法がない型安全な言語となっている。