Одинаковый синтаксис обеспечивает предложение, один успех, один сбой - PullRequest
Новая
       37

Одинаковый синтаксис обеспечивает предложение, один успех, один сбой

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

Этот раздел напоминает мне «Связанное местоположение 1. Это постусловие, которое может не сохраняться». 

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
method n_RecvGntSinv__2_0(Cache_Data:array<DATA>,   Cache_State:array<CACHE_STATE>,   Chan2_Cmd:array<MSG_CMD>, Chan2_Data:array<DATA>,i:nat, N0:nat,p__Inv0:nat,p__Inv2:nat)
requires Cache_Data.Length==N0
requires Cache_State.Length==N0
requires Chan2_Cmd.Length==N0
requires Chan2_Data.Length==N0
requires 0<= i<N0
requires p__Inv0!=p__Inv2&&p__Inv2<N0&& p__Inv0<N0
requires i==p__Inv2
requires (!((Cache_State[p__Inv0] == E) && (Chan2_Cmd[p__Inv2] == GntS)))//3
//guard condition
requires (Chan2_Cmd[i] == GntS)
ensures   !((Cache_State[p__Inv2] == S) && (!(Cache_State[p__Inv0] == I)) && (!(Cache_State[p__Inv0] == S)))
modifies Cache_Data
modifies Cache_State
modifies Chan2_Cmd
modifies Chan2_Data
{
  Cache_State[i] := S;
  Cache_Data[i] := Chan2_Data[i];
  Chan2_Cmd[i] := Empty;
}

Когда я меняю условие гарантии, как показано ниже, фрагмент 

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
method n_RecvGntSinv__2_0(Cache_Data:array<DATA>,   Cache_State:array<CACHE_STATE>,   Chan2_Cmd:array<MSG_CMD>, Chan2_Data:array<DATA>,i:nat, N0:nat,p__Inv0:nat,p__Inv2:nat)
requires Cache_Data.Length==N0
requires Cache_State.Length==N0
requires Chan2_Cmd.Length==N0
requires Chan2_Data.Length==N0
requires 0<= i<N0
requires p__Inv0!=p__Inv2&&p__Inv2<N0&& p__Inv0<N0
requires i==p__Inv2
requires (!((Cache_State[p__Inv0] == E) && (Chan2_Cmd[p__Inv2] == GntS)))//3
//guard condition
requires (Chan2_Cmd[i] == GntS)
ensures !((Cache_State[p__Inv2] == S) && (Cache_State[p__Inv0] == E ))modifies Cache_Data
modifies Cache_State
modifies Chan2_Cmd
modifies Chan2_Data
{
  Cache_State[i] := S;
  Cache_Data[i] := Chan2_Data[i];
  Chan2_Cmd[i] := Empty;
}

Это компилирует успех. Есть ли место, где я не понимаю Дафни?

...