Еще дафнячного: алиасинг

[kouzdra]

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

method inc (a: array, b: array, lo: int, hi: int)
requires 0 <= lo <= hi <= a.Length;
requires a.Length == b.Length;
modifies b;
{
ghost var prevElements := a[..];
var i := 0;
while i < a.Length
invariant a[lo..hi] == prevElements[lo..hi];
{
if i < lo || i >= hi {
b [i] := b [i] + 1;
}
i := i + 1;
}
}
Ну и:

var a := new int[6];
forall i | 0 <= i < a.Length {
a [i] := (i + 1) * 10;
}
...
inc (a, a, lo, hi);
Компилируется и нормально работает. Однако если мы уберем условие инкремента:

method inc (a: array, b: array, lo: int, hi: int)
requires 0 <= lo <= hi <= a.Length;
requires a.Length == b.Length;
modifies b;
{
ghost var prevElements := a[..];
var i := 0;
while i < a.Length
invariant a[lo..hi] == prevElements[lo..hi];
{
b [i] := b [i] + 1;
i := i + 1;
}
}
Оно заругается - поскольку если a == b, понятно что это некорректно. Сама функция лечится добавлением условия что такого быть не должно:

method inc (a: array, b: array, lo: int, hi: int)
requires 0 <= lo <= hi <= a.Length;
requires a.Length == b.Length;
requires a != b;
modifies b;
...
Но тогда как и следовало ожидать идет ругань на

inc (a, a, lo, hi);
На тему что а должно быть не равно a. После "раздвоения" массивов ошибка естественно пропадает.