Блог

Когда я запускаю свой код, я получаю ошибку index out of range. Та же проблема возникает и в ensures инструкции.

Мой код:

 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
}    

class TopC{
var
AuxData : DATA,
MemData : DATA,
CurPtr : NODE,
CurCmd : MSG_CMD,
ExGntd : boolean,
ShrSet : array<boolean>,
InvSet : array<boolean>,
Chan3 : array<class_0 > ,
Chan2 : array<class_0 > ,
Chan1 : array<class_0 > ,
Cache : array<class_1 > }    

method n_RecvInvAck(top:TopC,i:nat, N0:nat,p1:nat,p2:nat )
requires 0<= i<N0
requires top.Chan3.Length ==N0
 requires top.ShrSet.Length ==N0
 requires N0>0
requires 0<= p1 <top.Chan3.Length
requires 0<= p2 <top.Chan3.Length
requires p1
 requires N0>0
requires (i==p2)
requires   ((top.Chan3[i].Cmd == InvAck) amp;amp; (!(top.CurCmd == Empty)))
modifies top.Chan3[i] 
modifies top.ShrSet
modifies top

ensures  (!((top.ShrSet[p1] == true) amp;amp; (top.ExGntd == true) amp;amp; 
  (top.ShrSet[p2] == true)))


{
  top.Chan3[i].Cmd := Empty;
  top.ShrSet[i] := false;
  if (top.ExGntd == true) {
    top.ExGntd := false;
    top.MemData := top.Chan3[i].Data;
  }
}
  

Проблема в том, что метод modifies top , что означает, что он может выделить совершенно другой массив для top.ShrSet , который может иметь разную длину.

Вы можете добавить строку

 ensures top.ShrSet == old(top.ShrSet)
  

перед другим ensures предложением, чтобы исправить эту проблему.