Spec＃

Spec#は、C#の拡張版。
基本的には、C#と同じ。
ソースファイルの拡張子は「.ssc」。
プロジェクトファイルの拡張子は「.sscproj」。

リンク

Spec# 公式サイト

http://research.microsoft.com/specsharp/

契約プログラミング

ensures

D言語で言う「事後条件(out)」。

private int EnsureCapacity (int min)
  ensures min <= 10;
  ensures result == 0;
{
  /* 関数を抜ける際にensuresの条件がチェックされる。 */
  min = 10;
  //min = 11; // これは事後条件にひっかかる。
  return 0;   // 戻り値が０であることも事後条件。
}

expose

契約の解除。

expose(this)
{
  // この間で、契約を一時的に解除することができる。
}

んー？　exposeはprivateにできるのかな？？

invariant

D言語で言う「不変条件(invariant)」。

invariant 0 <= _size && _size <= _items.Length;

クラスのオブジェクトが生成されてから、死ぬまでの条件。

invariant forall

D言語で言う「不変条件(invariant)」。

invariant forall { int i in (_size : _items.Length); _items[i] == null };

クラスのオブジェクトが生成されてから、死ぬまでの条件。
一時的な変数に置きなおされても大丈夫なようにしている・・・・のかな？

requires

D言語で言う「事前条件(in)」。

public virtual int BinarySearch (int index, int count, object value, IComparer comparer)
    requires 0 <= index;
    requires 0 <= count;
    requires index + count <= Count;

otherwise

各契約条件に失敗したときの動作を記述する。

public virtual int BinarySearch (int index, int count, object value, IComparer comparer)
    requires 0 <= index otherwise ArgumentOutOfRangeException;
    requires 0 <= count otherwise ArgumentOutOfRangeException;
    requires index + count <= Count otherwise ArgumentException;

コンパイル時のデータチェック

nullチェック

次のコードは、initialElementsがnullの可能性がある。
Spec#のコンパイラは、コンパイル時にnull参照の可能性がある変数を警告してくれる。

 public Bag(int[] initialElements) {
   this.count = initialElements.Length;
 }

また簡易的にnullチェックを行う方法もある。

null禁止

次のように、nullを防ぎたい変数に「！」をつけることでnullを禁止できる。

 public Bag(int[] ! initialElements) {
   this.count = initialElements.Length;
 }