インターフェイス不変剤の時間的論理

Question

インターフェイスで不変剤を表現するためのある種の時間論的論理を探しています。インターフェイスではデータ表現を指定していないため、invariantsはインターフェイスの公開されている関数のみに依存する必要があります。

たとえば、単純なインターフェイス（Javaスタイル）の合計があるとします。

interface Sum {
    public void add (int a);
    public int getSum();
}

不変で表現したいと思います getSum の合計を返します a すべての呼び出しで add(a), 、この合計のデータ表現を使用せずに。

これを行うことを考えることができる唯一の方法は、何らかの形の時間論的論理を使用することです。私が読むことができるこのテーマに関する文献はありますか？どんなポインターも大歓迎です。

Answer 1

標準的な方法は、いわゆる使用を使用することです ゴースト変数. 。ゴースト変数は、仕様にのみ表示される場合を除き、通常の変数のようなものです（実際に実行するプログラムの一部ではありません）。言い換えれば、ゴースト変数は元のプログラムには存在しません。仕様によって追加されます。前提条件、事後条件、および不変性は、ゴースト変数を参照することが許可されています。

直感的には、ゴースト変数を使用すると、過去に呼び出された方法について状態を維持できます。これらのメソッドの仕様はゴースト変数を更新することができ、この情報を覚えています。

ゴースト変数を追加することで、特定の課題の問題を解決できます totalSoFar. 。次に、次のように、各メソッドに適切な仕様を追加します。

interface Sum {
    ghost int totalSoFar = 0;

    /* postcondition: totalSoFar = old(totalSoFar) + a */
    public void add (int a);

    /* postcondition: returnvalue = totalSoFar */
    public int getSum();
}

どのようにポストコンディショニングがあるかに注意してください add() に渡されたパラメーターに基づいて、ゴースト変数を更新します add(). 。同様に、の条件 getSum() Ghost変数の観点からのリターン値について説明します。

これが標準パターンです。ゴースト変数を使用して、必要な状態を追跡します。この状態を修正する方法については、条件付けを書いてゴースト変数の状態を更新します。ゲッターの場合、ゴースト変数の状態の観点から結果を表現します。

Answer 2

何をするにしても、あなたの仕様は、オブジェクト内のアキュムレータを反映した内部状態を持つことが判明します。このシンプルなクラスの場合、仕様は実装よりも簡単ではありません。ポイントは、はるかに複雑なケースでは、仕様がより単純であるということです。キーの下にデータを追加し、後で取得できる辞書を考えてみましょう。仕様は、キー/値のペアの線形配列に相当する可能性があり、検索は簡単な線形検索です。実装は、おそらくハッシュまたはバランスの取れたバイナリツリーに基づいたスキームです。 仕様 推論するのは簡単です、あなたはあなたを証明します 実装 仕様と同じように動作すると、設定されます。明日は、実装を引き裂き、それをいくつかのよりファンシーな構造に置き換え、仕様に準拠していることを再度証明します。他の場所に変更はありません。

仕様は、基本的に同じプログラムを別の（できれば扱いやすい）プログラミング言語で再び書き込み、おそらくパフォーマンスの考慮事項を上本し、両方のプログラムが同じことをすると推論しています。最新の仕様言語が判明しました 多くの 通常のプログラミング言語（および仕様にもバグがある可能性があります...）よりも使用するのは難しく、それらが同じように振る舞うという証拠は、心の弱い人ではありません。そして、私のプログラムがどのように振る舞うべきかについてのアイデアを思いつき、それをプログラムするなら、それは仕様と最終プログラムが同じ誤解とコーナーケースを逃したという理由で理由に耐えます。 「プログラム検証」運動の壮大な失敗がありました。ベリーの「ソフトウェアエンジニアリング分野の学問的正当性」を見てください（CMU/SEI-92-TR-34）数十行のプログラムの例では、書かれた「証明された」ことを証明し、修正して再度検証しました 学術雑誌に出版されています この地域の最大の専門家の何人かによって数回、それは各ラウンドでした。