2

2 つの外部関数 init() と revoke() があるとします。Init() は「有効な」値を返し、revoke() はそれらを無効にします。use() が、初期化されているが取り消されていない値のみを使用していることを確認したいと思います。このプロパティを述語 (ランダムなセッション ID と考えてください) またはそれ以外として説明する方法がわかりません。

#include <lib.h>

// "ensures valid_val(\result)"
extern int init();
extern revoke(int);

/*
 @ assigns \nothing;
 @ require valid_val(val);
 */
void use(int val) {
    ...
}

int main() {
    int v = init();
    use(v);
    revoke(v);
}
4

1 に答える 1

3

実際、このプロパティを単一のACSL述語として表現することはできません。実際、それはプログラムの実行全体に依存します。Aoraiプラグインを使用すると、許可された一連の関数呼び出しをオートマトンの形式で表現できますが、必要なものを完全にキャプチャすることはできません。より正確には、トークンの存続期間が重複するシナリオを表現することはできません（ただし、例の主な機能が正しいことを証明するには完全に十分です）。

とは言うものの、少しの計装で、一般的な仕様を思い付くことができるはずです。最初のトリックは、対応するインデックスが有効なトークンである場合にセルがゼロ以外の（ゴースト）配列を宣言することです。

typedef int token;

/*@ ghost extern int valid_token[]; */

/*@ predicate is_valid(token t) = valid_token[t] != 0; */

/*@ 
  assigns valid_token[\at(\result,Post)];
  ensures is_valid(\result);
*/
extern token init();

/*@
  requires is_valid(t);
  assigns valid_token[t];
  ensures !is_valid(t);
*/
extern revoke(token t);

/*@
 @ requires is_valid(val);
 @ assigns \nothing;
 */
void use(token val) {

}

/*@ requires \forall token t; !is_valid(t); */
int main() {
    token v = init();
    use(v);
    revoke(v);
}

サイズが定義されていない配列を使用するという事実が少し怪しいと思われる場合、ほぼ純粋なACSLソリューションは、次のように、真理値がinitおよびrevokeによって変更される状態に依存する未定義の述語を使用することです。

 typedef int token;

/*@ ghost int glob_state; */

/*@ axiomatic validity {
  predicate valid_token{L}(token t) reads glob_state;
}
*/

/*@ predicate unchanged_token{L1,L2}(token t) =
  \forall token t1; t!=t1 ==> 
  valid_token{L1}(t1) <==> valid_token{L2}(t1);
*/

/*@ 
  assigns glob_state;
  ensures valid_token(\result);
  ensures unchanged_token{Pre,Here}(\result);
*/
extern token init();

/*@
  requires valid_token(t);
  assigns glob_state;
  ensures !valid_token(t);
  ensures unchanged_token{Pre,Here}(t);
*/
extern revoke(token t);

/*@
 @ requires valid_token(val);
 @ assigns \nothing;
 */
void use(token val) {

}

/*@ requires \forall token t; !valid_token(t); */
int main() {
    token v = init();
    use(v);
    revoke(v);
}

割り当てる関数がglob_state述語を変更する場合があります。実際、引数の1つの値に対してのみ変更されるため、すべてのトークンの有効性を示す補助述語は、との間L1で同じままL2です。

于 2012-08-29T16:07:14.927 に答える