Spec# （ちょっと追加）

すぐ下 に書いた Spec# ですが、 名無しさん♯ に教えていただいた（どうもです）
http://research.microsoft.com/projects/T5/ppt/SpecSharpShort.ppt
を見ると確かに VS.NET 2003 らしきもので動いてますね。

それと、よくわからないと書いた object invariant ですが、この PPT を見てなんとなくわかりました。

　　class T {
　　　　int[] bufferInt;
　　　　bool[] bufferBool;
　　　　invariant bufferInt.Length == bufferBool.Length;

みたいに整合性のチェックを指定できるようです。
ただ、「いったいどのタイミングでチェックするのよ」 という問題があります。複数スレッドから同時アクセスされる可能性まで考慮すると、自動的に適切なタイミングでチェックすることは非常に難しくなります。そこで、expose (o) { . . . } という構文も追加されているということなようです。

なるほどです。method contracts と object invariants をきちんと使用すれば、インスタンスが正常な状態に保たれているかをかなり正確にチェックすることができそうです。むしろ問題は、正確なチェックをするような method contracts や object invariants を書けるかどうかかなぁ(^^;