kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Category:

Собственно пример на инварианты в dafny:

Раз уж пошло такое - иллюстрация к этому: https://kouzdra.livejournal.com/4407243.html
Вот такой код компилируется и работает:
var lo, hi := 2, 4;
var a := new int[6];
forall i | 0 <= i < a.Length {
  a [i] := (i + 1) * 10;
}
ghost var prevElements := a[..];
var i := 0;
while i < a.Length
  invariant a[lo..hi] == prevElements[lo..hi];
{
  if i < lo || i >= hi {
    a [i] := a [i] + 1;
  }
  i := i + 1;
}
А если заменить
if i < lo || i >= hi {
  a [i] := a [i] + 1;
}
на
if i <= lo || i >= hi {
  a [i] := a [i] + 1;
}
Компилятор выдает ошибку о нарушении инварианта цикла.

PS: Замечу, кстати что на ошибку, которую я реально сделал: написал
while i <= a.Length
вместо
while i < a.Length
Компилятор тоже выругался - по той же причине: для индекса i массива a должно выполняться условие
0 <= i < a.Length
Tags: dafny, verification, Компутерщина, Языки программирования
Subscribe

  • Нафиг - нафиг...

    Мое отношение к "медицине" определяется тем, что она силком вытягивает из меня уже лет 35 довольно приличные деньги на свои "услуги". При этом на…

  • My comment to an entry 'Снова все о том же: вакцинация от Ковида' by mary_spiri

    Я полагаю все эти меры никак не оправдываемыми их результатом. Я сам не очень молодой — 55 — и подогаю риск смерти от вируса незначимым по сравнению…

  • Это жжж неспроста

    Йебанутые собачники - это все-таки диагноз: Водокачкин был заметен ебанутым собачничеством и любовью к "ножичкам". Тут вдруг разразился тоже…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 15 comments

  • Нафиг - нафиг...

    Мое отношение к "медицине" определяется тем, что она силком вытягивает из меня уже лет 35 довольно приличные деньги на свои "услуги". При этом на…

  • My comment to an entry 'Снова все о том же: вакцинация от Ковида' by mary_spiri

    Я полагаю все эти меры никак не оправдываемыми их результатом. Я сам не очень молодой — 55 — и подогаю риск смерти от вируса незначимым по сравнению…

  • Это жжж неспроста

    Йебанутые собачники - это все-таки диагноз: Водокачкин был заметен ебанутым собачничеством и любовью к "ножичкам". Тут вдруг разразился тоже…