Экспоненциальный метод в dafny: инвариант может не поддерживаться

Question

Я начал изучать Дафни, и я только изучил инварианты. У меня есть этот код:

function pot(m:int, n:nat): int
{
  if n==0 then 1
  else if n==1 then m
  else if m==0 then 0
  else pot(m,n-1) * m
} 
method Pot(m:int, n:nat) returns (x:int)
ensures x == pot(m,n)
{
  x:=1;
  var i:=0;
  if n==0 {x:=1;}
  while i<=n
  invariant i<=n;
  {
    x:=m*x;
    i:=i+1;
  }
}

И данная ошибка заключается в следующем: "Этот инвариант цикла может не поддерживаться циклом". Я думаю, что мне может понадобиться другой инвариант, но я думаю, что мой код является правильным, кроме этого (я думаю). Любая помощь приветствуется. Заранее спасибо.

Answer 1

Инвариант цикла должен выполняться всякий раз, когда оценивается условие ветвления цикла. Но на последней итерации вашего цикла, i на самом деле будет n+1, то есть инвариант цикла неверен.

Изменение инварианта цикла на i <= n + 1 или изменение состояния ветви цикла на i < n исправит эту конкретную проблему.

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