Еще дафнячного: алиасинг: 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. После "раздвоения" массивов ошибка естественно пропадает.

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

"И все его оставили"

Технологии

Попались обсуждения какого-то

Error