Dafny недостаточно читает предложение для чтения элемента массива

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 Cache : array<class_1 > }

predicate  inv__1(top:TopC,N1:nat,p__Inv0:nat, p__Inv2:nat)
  reads top
  reads top.Cache[p__Inv0]
  eads top.Cache[p__Inv2]
  requires top.Cache.Length ==N1
  requires N1>0
  requires top.Cache.Length ==N1
  requires N1>0
  requires 0<= p__Inv0<N1
  requires 0<= p__Inv2<N1
  {
(!((top.Cache[p__Inv2].State == E) && (!(top.Cache[p__Inv0].State == I))))
}

Это мой тестовый код, когда я его компилирую, нахожу ошибку: недостаточное предложение чтения для чтения элемента массива в строке «reads top.Cache[p__Inv0]», я не понимаю, где я ошибаюсь, может ли аннотация чтения не использоваться в элементе массива?


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

Ответы (1)


arrow_upward
0
arrow_downward

Функция (включая предикат, возвращающий bool) должна объявлять объекты, от состояния которых она зависит. Предикат inv__1 зависит от

  • состояние объекта top, так как функция использует поле .Cache этого объекта
  • состояние массива top.Cache, так как функция использует элементы этого массива
  • состояние объектов top.Cache[p__Inv2] и top.Cache[p__Inv0], так как функция использует поле .State этих объектов

Итак, функции нужен следующий кадр чтения:

reads top
reads top.Cache
reads top.Cache[p__Inv0], top.Cache[p__Inv2]

Это второй из них, который отсутствует в вашей программе.

Если вы никогда не собираетесь изменять сам массив Cache, вы можете объявить его как константу после построения:

const Cache: array<class_1>

Тогда вам не нужно включать top.Cache в кадр чтения.

person Rustan Leino    schedule 14.04.2020