очевидный инвариант терпит неудачу в Дафни - PullRequest
Новая
       42

очевидный инвариант терпит неудачу в Дафни

0 голосов
/ 11 апреля 2020 
  datatype CACHE_STATE = I| S| E
  datatype MSG_CMD = Empty| ReqS| ReqE| Inv| InvAck| GntS| GntE
  type NODE=nat
  type DATA=nat
type boolean=bool

class  class_0  {
var 
Data : DATA,
Cmd : MSG_CMD
}


class  class_1  {
var 
Data : DATA,
State : CACHE_STATE
}





method n_RecvGntSinv__1_2( 
Chan2 : array<class_0 > , 
Cache : array<class_1 > ,i:nat, N1:nat ,p__Inv0:nat,p__Inv2:nat)
modifies Chan2[i]
modifies Cache[i]
requires 0<= i<N1

requires Cache.Length ==N1
requires N1>0

requires Chan2.Length ==N1


requires p__Inv0!=p__Inv2&&p__Inv2<N1&& p__Inv0<N1

requires Chan2[i] != null
requires Cache[i] !=null

requires i!=p__Inv0&&i!=p__Inv2
requires (!((Cache[p__Inv2].State == E) && (!(Cache[p__Inv0].State == I)))) 
requires   (Chan2[i].Cmd == GntS)



 ensures Cache==old(Cache)
 ensures Chan2==old(Chan2)

ensures   (!((Cache[p__Inv2].State == E) && (!(Cache[p__Inv0].State == I))))

{
  Cache[i].State := S;
  Cache[i].Data := Chan2[i].Data;
  Chan2[i].Cmd := Empty;
}

Я поставил требование i отличается от p__Inv2 и p_Inv0, поэтому назначения не должны мешать оценке инварианта.

Очевидно, что инвариант (! ((Cache [p__Inv2] .State == E) && (! (Cache [p__Inv0] .State == I)))) должен храниться, если он выполняется до выполнения .

Дафни показывает, что мои утверждения ошибочны, и приводит контрпример, которого я не могу понять.

1 Ответ

0 голосов
/ 13 апреля 2020

Ваше предварительное условие допускает возможность того, что Cache[i] ссылается на тот же объект, что и Cache[p__Inv0] или Cache[p__Inv2]. Если это именно то, что вы намеревались, то тело метода действительно неверно, как сообщает верификатор. Если это не то, что вы хотели, то предварительное условие типа 

requires forall j,k :: 0 <= j < k < Cache.Length ==> Cache[j] != Cache[k]

заставит ваш метод проверить.

...