CODEWITHSUNDEEP
dafny
Hongjian Jiang
Hongjian Jiang

Reputation: 297

The same syntax ensure clause,one success,one fail

This section reminders me "Related location 1. This is the postcondition that might not hold."

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;
}

When i change the condition of ensure,like the below fragment

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;
}

This compiles success.Whether there are some place i don't understand Dafny?

Upvotes: 0

Views: 95

Answers (1)

yongjianLi
yongjianLi

Reputation: 23

I think Dafny is no longer maintained by people, it is dead! No need to use it!

Upvotes: 0

Related Questions