Проверка Dafny - обратитесь к оригинальному var в состоянии post

Question

Я пытаюсь проверить свой код в Dafny, и у меня возникла проблема: У меня есть метод, который выполняет итерацию по последовательности и меняет ее. Метод изменяет последовательность в соответствии с элементами в последовательности. Я хотел бы добавить условие сообщения следующим образом: «если элементы в последовательности X, то что-то должно произойти». Проблема в том, что метод изменяет набор (добавляет элемент и т. Д.), И я хочу проверить состояние исходной последовательности. Есть ли элегантный способ сделать это в Дафни? (Единственный способ, о котором я мог думать сейчас, - сохранить глобальный var исходного состояния последовательности, но я ищу правильный способ сделать это).

Пример кода:

method changeSeq(p: class1, s: seq<class1>) 
ensures |s| == 10 ==> p in s 
{ 
    if (|s| == 10){ 
     s := s + [p]; 
    } 
} 

В коде, я хочу пост состояние проверить оригинал s стат, а не его стат после того как мы изменили его.

Answer 1

вы можете использовать old для старого значения переменной, например s == old(s).

Вот один пример: http://rise4fun.com/Dafny/fhQgD

От Dafny Documentation 22.18. Old Expressions

OldExpression_ = "old" "(" Expression(allowLemma: true, allowLambda: true) ")"

старое выражение используется в постусловий. old(e) оценивает выражение значения e имело при входе в текущий метод. Обратите внимание, что старый влияет только на разрывы кучи, такие как o.f и a[i]. В частности, старый не влияет на значение, возвращаемое для локальных переменных или out-parameters.