Для удовлетворения в Дафни

Меня смущает оператор forall Дафни, если оператор внутри forall предназначен для обновления переменной, такой как c.arr[i].d, которая смешивается с доступом к полю и элементу массива. Например, следующий пример не может быть скомпилирован.

Я думаю, что явное указание модифицирующего предложения очень утомительно, мне нужно указать: модифицирует top, модифицирует top.Cache[i]

 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_RecvReqS(top:TopC,i:nat, N0:nat )
requires 0<= i<N0
requires top.Chan1.Length ==N0
 requires N0>0
   requires top.InvSet.Length ==N0
 requires N0>0
 requires top.ShrSet.Length ==N0
 requires N0>0
  requires top.Cache.Length ==N0

requires   ((top.Chan1[i].Cmd == ReqS) && (top.CurCmd == Empty))


modifies top.Chan1[i]
modifies top.InvSet
modifies top.ShrSet
modifies top
modifies top.Cache


{
  top.CurCmd := ReqS;
  top.CurPtr := i;
  top.Chan1[i].Cmd := Empty;


  forall j  | 0<= j< N0 {
    top.InvSet[j] := top.ShrSet[j];

  }

  forall j  | 0<= j< N0 {
    top.Cache[j].State:= I;

  }

}

dafny
person yongjianLi    schedule 17.04.2019    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Знание о влиянии метода на кучу имеет решающее значение для проверки, хотя написание предложений modifies может быть утомительным. В вашем случае вам необходимо учитывать все модификации, которые выполняет метод n_RecvReqS. Как вы заметили, сюда входят все объекты top.Cache[j] для всех j.

Один из способов включить их в предложение modifies — использовать понимание множества:

modifies set j | 0 <= j < top.Cache.Length :: top.Cache[j]

Это обозначает набор объектов top.Cache[j], где j находится среди значений, удовлетворяющих 0 <= j < top.Cache.Length.

Читайте дальше, чтобы узнать о дополнительных возможностях.

Если вы делаете это часто и считаете, что все эти кеши являются частью представления объекта TopC, то вы, вероятно, захотите абстрагироваться от многих частей вашего состояния и поместить их в набор. Если вы ищете в наборе тестов Dafny такие объявления, как

ghost var Repr: set<object>

вы найдете несколько примеров. Тогда весь ваш пункт modifies будет просто

modifies Repr

Если вы еще не готовы использовать такой набор Repr, то есть еще одно простое предложение modifies, которое вы можете написать для модификаций кеша в вашей программе. Если вы перечислите последовательность объектов в предложении modifies, Дафни автоматически преобразует ее в соответствующий набор объектов. Вы можете преобразовать все элементы массива top.Cache в последовательность с помощью выражения top.Cache[..]. Таким образом, чтобы учесть обновления в вашем заявлении forall, вы можете написать

modifies top.Cache[..]

К сожалению, Дафни не понимает автоматически, что каждое top.Cache[j] в теле вашего оператора forall действительно является элементом множества, сформированного из последовательности top.Cache[..]. Можно помочь верификатору доказать это, но это внесет некоторый беспорядок в оператор forall. Вот как я это сделал:

forall j | 0 <= j < N0 {
  (assert top.Cache[j] in top.Cache[..]; top.Cache[j]).State:= I;
}

Рустан

person Rustan Leino    schedule 18.04.2019