事後条件をチェックすると結果が変わるプログラム

事後条件のチェックを行うかどうかによって結果が変わる関数を思いつきました。

class TestBreaker

instance variables
private x: int := 0;

operations
public 破壊的操作: () ==> bool
破壊的操作() == (x := x+1; return true);

functions
public Test: int -> int
Test(a) == self.x + a
post self.破壊的操作();

end TestBreaker

以下のようにオブジェクトを生成し、関数を呼び出します。

>> create t:=new TestBreaker()
>> print t.Test(0)
>> print t.Test(0)
>> print t.Test(0)

事後条件のチェックを行わないときには0, 0, 0 が返りますが、チェックを行った
ときには、0, 1, 2 の値が返ります。

このプログラムもVDMToolsも問題ないですよね？現状の言語仕様ではこんなプログラムも作れてしまいます。事前条件、不変条件でも作れるでしょう。
通常はこんな仕様はありえないのですが、それを禁止するor検出する手段もありません（多分）。