LHS присваивания должен обозначать изменяемую переменную

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_SendGntEinv__5_0(Cache_State:array<CACHE_STATE>,   Chan2_Cmd:array<MSG_CMD>,   Chan2_Data:array<DATA>, CurCmd:MSG_CMD, CurPtr:NODE, ExGntd:boolean, MemData:DATA, ShrSet:array<boolean>,   
i:nat,N0:nat,p__Inv0:nat,p__Inv2:nat)
requires 0<= i < N0
requires Chan2_Cmd.Length==N0
requires Chan2_Data.Length==N0
requires ShrSet.Length==N0
requires p__Inv0!=p__Inv2&&p__Inv2<N0&& p__Inv0<N0
requires i==p__Inv2
//1
//guard condition
requires ((Chan2_Cmd[i] == Empty) && (CurCmd == ReqE) && (CurPtr == i) && (ExGntd == false) && (forall j  |0<= j<N0 :: (ShrSet[j] == false) ))
ensures   (!((Cache_State[p__Inv0] == E) && (Chan2_Cmd[p__Inv2] == GntS)))
modifies Chan2_Cmd
modifies Chan2_Data
modifies ShrSet
{
  Chan2_Cmd[i] := GntE;
  Chan2_Data[i] := MemData;
  ShrSet[i] := true;
  ExGntd := true;
  CurCmd := Empty;
}

Я пытаюсь скомпилировать этот код, однако подсказка упоминает меня

LHS присваивания должен обозначать изменяемую переменную

и я не знаю, как решить проблему. Должны ли CurCMD и EXGntd быть значением массива или есть другое решение этой проблемы?


dafny
person sword    schedule 21.04.2020    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Внутренние параметры являются неизменяемыми. Сообщение об ошибке указывает, что вы пытаетесь назначить им.

Вы можете ввести (изменяемые) локальные переменные, если хотите. В вашем примере это будет выглядеть так:

var ExGntd', CurCmd' := ExGntd, CurCmd;
...
ExGntd' := true;
CurCmd' := Empty;
person Rustan Leino    schedule 21.04.2020