Как выписать decreases, если на разных итерациях убывают разные величины

Здесь будет очень кратко показано, как получать decreases в описанных в заголовке сообщения случаях. На самом деле предлагаемая здесь техника может быть применена и при решении задач на методы Флойда на зачете.



Исходная постановка задачи: требуется доказать завершимость такой программы:

method Test(SomeRandom:seq<int>)
requires |SomeRandom|==5;
requires forall k:int :: 0<=k<|SomeRandom| ==> 0<SomeRandom[k]<10;
{
 ghost var c:int := 1;
 ghost var Pos:nat := 0;
 ghost var Max := |SomeRandom|;
 
 while(c!=0)
 {
  if(Pos<Max-1) {
   c := SomeRandom[Pos];
   Pos := Pos+1;
  } else {
   c := 0;
  }
 }
}

Dafny говорит

cannot prove termination; try supplying a decreases clause for the loop

Т.е. он просит нас написать decreases. Если бы Pos увеличивался на каждой итерации, то decreases пишется вполне очевидно: decreases Max-Pos; Но в данном случае на последней итерации цикла уменьшения Max-Pos не происходит. Но мы знаем, что при этом убывает c. Попробуем написать тогда такой decreases :

method Test(SomeRandom:seq<int>)
requires |SomeRandom|==5;
requires forall k:int :: 0<=k<|SomeRandom| ==> 0<SomeRandom[k]<10;
{
 ghost var c:int := 1;
 ghost var Pos:nat := 0;
 ghost var Max := |SomeRandom|;
 
 while(c!=0)
          decreases if Pos<Max-1 then Max-Pos else c;
 {
  if(Pos<Max-1) {
   c := SomeRandom[Pos];
   Pos := Pos+1;
  } else {
   c := 0;
  }
 }
}

Запускаем Dafny:

decreases expression might not decrease
decreases expression must be bounded below by 0 at end of loop iteration

Получили аж два сообщения об ошибках. Второе исправить просто: Dafny надо явно сказать, что c >= 0 :

method Test(SomeRandom:seq<int>)
requires |SomeRandom|==5;
requires forall k:int :: 0<=k<|SomeRandom| ==> 0<SomeRandom[k]<10;
{
 ghost var c:int := 1;
 ghost var Pos:nat := 0;
 ghost var Max := |SomeRandom|;
 
 while(c!=0)
          invariant 0 <= c;
          decreases if Pos<Max-1 then Max-Pos else c;
 {
  if(Pos<Max-1) {
   c := SomeRandom[Pos];
   Pos := Pos+1;
  } else {
   c := 0;
  }
 }
}

Запускаем Dafny и убеждаемся, что второе сообщение исчезло, а первое всё равно осталось. Попробуем разобраться более детально, в чем дело.

Для начала вспомним, что означает правильный decreases. decreases помечает некоторое целочисленное выражение. Это выражение вычисляется перед каждой итерацией и запоминается. Перед следующей итерацией оно будет вычислено вновь и должно быть меньше, чем то значение, которое запоминалось ранее. Какая ситуация у нас: попробуем расписать значения переменных (Pos и c) на каждой итерации:

начало цикла: Pos == 0, c == 1

Pos == 1, c == чтотоположительное

Pos == 2, c == чтотоположительное

. . .

Pos == Max-2, c == чтотоположительное

Pos == Max-1, c == чтотоположительное

Pos == Max-1, c == 0

конец цикла!

А теперь надо подобрать такое выражение, одно для каждой итерации (т.е. одно для каждой выписанной строчки), чтобы его значение уменьшалось. Между итерациями

Pos == k, c == чтотоположительное

Pos == k+1, c == чтотоположительное

Это выражение есть, конечно, "Max - Pos" . Про с нам тут думать не надо.

А если Pos == Max-1, то выражение должно быть равно "с", т.к. оно убывает.

В результате, первая прикидка на выражение у decreases получается такой:

decreases if Pos < Max-1 then Max-Pos else c;

Хм, получилось почти то, что было раньше. Что-то тут явно не так. И действительно на последней итерации это выражение равно 0, на предпоследней равно "чтотоположительное", а на предпредпоследней равно "2". С какой это стати "чтотоположительное" должно быть меньше двух? В чем же причина ошибки? Ошибка в том, что мы некорректно указали, к каким итерациям какую ветвь if'а надо вычислять. А именно, все итерации, кроме последней, можно задать при помощи выражения Pos <= Max-1 && c > 0. Т.е. вторая прикидка на decreases получается такой:

decreases if Pos <= Max-1 && c > 0 then Max-Pos else c;

Смотрим: на последней итерации это выражение равно нулю, на предпоследней Max-Pos, т.е. единице! На предпредпоследней ... двойке. Ура, получилось! Проверим, что скажет Dafny:

Dafny program verifier finished with 2 verified, 0 errors

На самом деле ситуацию, когда есть несколько убывающих выражений, которые можно упорядочить так, чтобы убывание происходило лексикографически, т.е. либо на очередной итерации убывает первое выражение, либо оно сохраняет значение, но убывает второе значение, либо сохраняются первое и второе, но убывает третье и т.д. (при этом на следующей итерации третье выражение может увеличиться, но первое должно уменьшиться или, если первое сохранило значение, то должно уменьшиться второе), то decreases можно записать, перечислив эти выражения через запятую! Очень просто и наглядно. Так, в нашем случае получится следующий код на Dafny:

method Test(SomeRandom:seq<int>)
requires |SomeRandom|==5;
requires forall k:int :: 0<=k<|SomeRandom| ==> 0<SomeRandom[k]<10;
{
 ghost var c:int := 1;
 ghost var Pos:nat := 0;
 ghost var Max := |SomeRandom|;
 
 while(c!=0)
          invariant 0 <= c;
          decreases Max-Pos , c;
 {
  if(Pos<Max-1) {
   c := SomeRandom[Pos];
   Pos := Pos+1;
  } else {
   c := 0;
  }
 }
}