条件

引数の型は事前条件の一種だ。返値の型は事後条件の一種だ。と思いついてから検索したらEiffelが出てきた。
「厳密な事前／後条件が成り立っているかどうか」を調べるためには動作条件での検証が必要になるのだが、動作条件での検証では「事前／後条件が常に成り立っているかどうか」を調べることが難しい。そのため、強い型付きの言語では型整合性という「事前／後条件の必要条件が常に成り立っているかどうか」をコンパイル時に調べている。
もしも型が一般的パラメータ、javaのgenericsのような型パラメータではなく、を持っていれば、大半の事前／後条件は厳密に判定できるのではないだろうか。*1

  void method(int i){
    assert(0<=i&i<this.size);
    // do Something.
  }

↓コンパイル時に定まっている事前条件を型に繰り込んだ。*2

  void method(int[0,MaximumInteger] i){
    assert(i<this.size);
    // do Something.
  }

*1:単純なbit演算に還元出来ないのでコンパイルは遅くなるかも。同一型の間でだけ一般パラメータ判定を行うようにすれば良いのかな。

*2:パラメータの省略を許すようにすれば互換性が高くなるかな。