ソフトウェア技術のなかで僕が一番興味を持っているのは仕様技術です。正確に適切な仕様を記述すること、そしてその仕様をもとに検証ができること、それを望んでいるのですけど、まー、難しいですね、イロイロと。
で、仕様に関して最近思っていることなどを少し書いてみます。
「仕様を書く」という作業では、記述言語が必要ですね。その記述言語の基本単位を文（sentence）と呼びます。ここで、「文」という語は技術用語ですよ、なんとなく使っているわけでもないし、国語辞書的な用法でもないですからご注意。でも、「文」だけだと短すぎるので、以下「記述文」にします。
一番有名な記述文（の構文）はホーア式でしょう。事前条件P、実行部E、事後条件Qを組み合わせて {P}E{Q} という形で書きますが、現在のプログラミング言語との相性からは、中括弧の使用法を逆にして P{E}Q がいいと僕は思います（ので、こっちを使います）。P{E}Q の意味は、「条件Pを満たしている状態で、Eを実行したら、実行後には条件Qを満たす」というものです。
例えば、 (value() >= 0){inc();}(value() > 0) ならば、「value()が0以上の状態で、inc(); を実行したら、実行後にはvalue()は0より大きくなる」です。テストコードに直せば：
if (value() >= 0) {
inc();
if (value() > 0 ) {
return true;
} else {
return false;
}
} else {
return true;
}
このコードは仕様違反があったときにだけfalseを返します。事前条件が成立してないことは仕様違反ではないのでtrueを返すことに注意してください。事前条件を調整するのはテスターの仕事ですから、(value() >= 0)じゃないから仕様違反だ、は理不尽すぎますね。
[追記]このケースだと、(value() >= 0) が不変条件のような雰囲気がありますが、ほんとに不変条件なら、(true){}(value() >= 0) と書かないといけません。
（続く）
