Что знает Дафни о петлях с разрывом?

I am used to loops

while Grd
invariant Inv
{ ..}
assert Inv && !Grd;

без перерыва Дафни знает, что Inv && ! Grd верно, но: Дафни не проверяет инвариант цикла после команды break;. Следовательно

method tester(s:seq<int>) returns (r:int) 
ensures r <= 0
{   var i:nat := |s|;
    r := 0;
    while (i > 0)
       decreases i
       invariant r == 0;
    {   i := i -1;
        if s[i]< 0  { r:= s[i]; break;}        
    }    
   // assert r == 0; // invariant dose not hold
}

method Main() {
    var x:int := tester([1,-9,0]);
    print x,"\n";
}

Ясно, что Дафни понимает, что инвариант больше не выполняется. Может ли кто-нибудь сказать мне, что на самом деле знает Дафни.


iteration break dafny
person david streader    schedule 08.09.2020    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Если есть операторы break, условие после цикла является дизъюнкцией Inv && !Grd и условий, которые выполняются в соответствующих операторах break.

Вот более формальный ответ:

При отсутствии каких-либо резких выходов (типа break) из цикла знакомый способ доказательства тройки Хоара

{{ P }}
while Grd
  invariant Inv
{
  Body
}
{{ Q }}

состоит в том, чтобы доказать следующие три условия (я игнорирую завершение):

  1. Убедитесь, что инвариант цикла сохраняется при входе в цикл:
P ==> Inv
  1. Убедитесь, что инвариант цикла поддерживается телом цикла:
{{ Inv && Grd }}
Body
{{ Inv }}
  1. Убедитесь, что инвариант и отрицательная защита доказывают Q:
Inv && !Grd ==> Q

Позвольте мне перефразировать условия 1 и 2. Для этого я начну с того, что перепишу цикл while в повторяющийся цикл с перерывами:

loop
  invariant Inv
{
  if !Grd {
    break;
  }
  Body
}

(Другими словами, я использую loop как while true.) Вышеприведенное обязательство доказательства 1 теперь можно перефразировать как доказательство.

{{ Inv }}
if !Grd {
  break;
}
Body
{{ Inv }}

где вам не нужно доказывать что-либо дальше на любом пути, который достигает break. Обязательство доказательства 2 можно перефразировать двояко:

{{ Inv }}
if !Grd {
  break;
}
Body
{{ break: Q }}

под этим я подразумеваю, что вам не нужно ничего доказывать, если вы дойдете до конца ...Body, но вы должны доказывать Q в любой break.

То, что я только что сказал, также применимо, когда Body содержит другие операторы break. Вот как Dafny обращается с циклами (то есть условие 0 плюс перефразированные условия 1 и 2 плюс проверка завершения).

person Rustan Leino    schedule 09.09.2020
comment
Я должен чаще оставлять вопросы без ответа. Это отличный ответ! :) - person James Wilcox; 11.09.2020