Собственно пример на инварианты в 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