(ブログ Do Design Space の もし C# で形式的検証ができたら と同じ内容です。2014 年の投稿です。)
C# では、コンパイル時に静的にコードをチェックし、警告やエラーを通知してくれます。
例えば、次のようなものです。
1 つ目の例はステートメントの条件分岐により、そのスコープに到達できるかどうかを判定しています。
実行はでき、致命的ではないため、エラーではなく警告が通知されています。
2 つ目の例の where 句では、ジェネリック型に対する制約が指定されています。
現時点のコンパイラもそれなりに強力な判断能力を持っているとは思いますが、
もし C# のコンパイラがさらに空気を読んで賢くなったら、
どのようなプログラミング エクスペリエンスを実現できるのかを考えてみましょう。
実装のお題として「与えられた 2 つの整数を昇順に並べ替えるメソッド」という単純なものを設定し、
どうすればバグのないプログラミングができるかを考えます。
まず、並べ替えのメソッドが満たすべき条件は次の通りです。
- 実行結果が意図した順番に並んでいる
- 実行前の値のセットと実行後の値のセットが同じである
そこで、メソッドの実装を始める前に、メソッドのシグネチャでこれらの条件を表現してみます。
/*
* このプログラムには、架空の機能が含まれます。
*/
class Program
{
static void Main(string[] args)
{
var sorted = Sort(new TwoValues(2, 1));
}
// (架空の機能) 引数に対する高度な制約。
static OrderedTwoValues Sort(TwoValues v) where Sort(v).SetEquals(v)
{
// TODO: あとで実装。
throw new NotImplementedException();
}
}
// (架空の機能) null を代入できない型。
public class TwoValues where this != null
{
public int X { get; private set; }
public int Y { get; private set; }
public TwoValues(int x, int y)
{
X = x;
Y = y;
}
public bool SetEquals(TwoValues v)
{
return X == v.X ? Y == v.Y
: X == v.Y && Y == v.X;
}
}
public class OrderedTwoValues : TwoValues
{
// (架空の機能) 引数に対する高度な制約。
public OrderedTwoValues(int x, int y)
: base(x, y) where x <= y
{
}
}
int[] や List<int> の代わりに、TwoValues クラスを定義して 2 つの整数を表現しています。
また、TwoValues クラスを継承して、順序を保持する OrderedTwoValues クラスを定義します。
このコンストラクターにある where x <= y は、
静的チェックのレベルで引数が x <= y を満たした状態でコンストラクターを呼び出さなければ、
コンパイルがエラーとなることを意味することにします。
そして、並べ替えを表す Sort メソッドの引数を TwoValues 型、戻り値を OrderedTwoValues 型とします。
これにより、条件 1 が保証されます。
さらに、Sort メソッドに対する制約として where Sort(v).SetEquals(v) を追加します。
SetEquals メソッドは ISet<T>.SetEquals メソッドと同様、集合として等しいかどうかを判定します。
これにより、条件 2 が保証されます。
このように強力な制約を導入することで、メソッドのシグネチャだけで条件 1, 2 を表現できました。
ということは、コンパイルが成功するように実装するだけで、このメソッドにはバグが存在しないことが保証されます。
(上記の時点の実装では NotImplementedException が発生するため、条件 2 を満たさず、コンパイルはエラーとなります。)
では、いよいよ Sort メソッドの実装です。
static OrderedTwoValues Sort(TwoValues v) where Sort(v).SetEquals(v)
{
// コンパイルが成功するための実装。
return v.X <= v.Y
? new OrderedTwoValues(v.X, v.Y)
: new OrderedTwoValues(v.Y, v.X);
}
new OrderedTwoValues(v.X, v.Y) の部分は v.X <= v.Y を満たすスコープの中にいるため、
OrderedTwoValues コンストラクターの制約 x <= y を満たすはずです。
また、new OrderedTwoValues(v.Y, v.X) の部分は v.Y < v.X を満たすスコープの中にいるため、この制約を満たすはずです。
人間が数学の証明をするとき、具体的な数値を代入しなくても、変数のまま大小関係を判定します。
もしコンパイラがもう少し賢くなれば、この程度の判断は十分可能でしょう。
同様に、OrderedTwoValues コンストラクターの引数には、一方に v.X を、他方に v.Y を渡しているため、
Sort(v).SetEquals(v) を満たします。
ここで例えば return new OrderedTwoValues(0, 1) などと実装してしまうと、コンパイル エラーとなります。
というわけで、上記の実装によりコンパイルは成功し、同時に正しい実装であることが保証されます。
このような手法は形式的検証 (formal verification) と呼ばれ、バグが存在してはならないソフトウェアを作成するときなどに利用されます。
C# においても、そのうち Roslyn をベースとして形式的検証のできるコンパイラが登場するのではないでしょうか。