Dafny, массивы и мультимножества
От: WolfHound  
Дата: 29.04.16 15:21
Оценка: 27 (1)
Играюсь вот с этой штукой:
http://research.microsoft.com/en-us/projects/dafny/
Попробовать в браузере можно тут:
http://rise4fun.com/dafny/Hello

Вот в этом коде дафна не может доказать первый ассерт. Но с моей точки зрения должна.
Это баг или я что-то не понимаю?
lemma TestMultiset(a : array<int>, begin : int, mid : int, end : int)
  requires a != null;
  requires 0 <= begin <= mid <= end <= a.Length;
{
  assert multiset(a[begin..mid]) + multiset(a[mid..end]) == multiset(a[begin..end]);
  assert a[begin..mid] + a[mid..end] == a[begin..end];
  assert |multiset(a[begin..mid])| + |multiset(a[mid..end])| == |multiset(a[begin..end])|;
  assert |a[begin..mid]| + |a[mid..end]| == |a[begin..end]|;
}

Без этого у меня квиксорт доказать не получается.
... << RSDN@Home 1.2.0 alpha 5 rev. 62>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Re: Dafny, массивы и мультимножества
От: Кодт Россия  
Дата: 06.05.16 14:57
Оценка:
Здравствуйте, WolfHound, Вы писали:

WH>Вот в этом коде дафна не может доказать первый ассерт. Но с моей точки зрения должна.
WH>Это баг или я что-то не понимаю?
WH>
WH>lemma TestMultiset(a : array<int>, begin : int, mid : int, end : int)
WH>  requires a != null;
WH>  requires 0 <= begin <= mid <= end <= a.Length;
WH>{
WH>  assert multiset(a[begin..mid]) + multiset(a[mid..end]) == multiset(a[begin..end]);
WH>  assert a[begin..mid] + a[mid..end] == a[begin..end];
WH>  assert |multiset(a[begin..mid])| + |multiset(a[mid..end])| == |multiset(a[begin..end])|;
WH>  assert |a[begin..mid]| + |a[mid..end]| == |a[begin..end]|;
WH>}
WH>

WH>Без этого у меня квиксорт доказать не получается.

А у тебя интервалы полуоткрытые или закрытые?
Для закрытых интервалов a[begin..mid] + a[mid..end] == a[begin..end] + a[mid], вообще-то.
Перекуём баги на фичи!
Re[2]: Dafny, массивы и мультимножества
От: WolfHound  
Дата: 06.05.16 15:17
Оценка:
Здравствуйте, Кодт, Вы писали:

К>А у тебя интервалы полуоткрытые или закрытые?
К>Для закрытых интервалов a[begin..mid] + a[mid..end] == a[begin..end] + a[mid], вообще-то.
Везде полуоткрытые.
Если бы были закрытые, то остальные ассерты тоже бы обломались. Вернее, дафна сказала бы что index out of range.
Дафна очень внимательная девушка. У неё не забалуешь.
... << RSDN@Home 1.2.0 alpha 5 rev. 62>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Re: Dafny, массивы и мультимножества
От: Буравчик Россия  
Дата: 15.05.16 23:01
Оценка: 32 (1)
Здравствуйте, WolfHound, Вы писали:

WH>Играюсь вот с этой штукой:
WH>http://research.microsoft.com/en-us/projects/dafny/
WH>Попробовать в браузере можно тут:
WH>http://rise4fun.com/dafny/Hello

WH>Вот в этом коде дафна не может доказать первый ассерт. Но с моей точки зрения должна.
WH>Это баг или я что-то не понимаю?
WH>
WH>lemma TestMultiset(a : array<int>, begin : int, mid : int, end : int)
WH>  requires a != null;
WH>  requires 0 <= begin <= mid <= end <= a.Length;
WH>{
WH>  assert multiset(a[begin..mid]) + multiset(a[mid..end]) == multiset(a[begin..end]);
WH>  assert a[begin..mid] + a[mid..end] == a[begin..end];
WH>  assert |multiset(a[begin..mid])| + |multiset(a[mid..end])| == |multiset(a[begin..end])|;
WH>  assert |a[begin..mid]| + |a[mid..end]| == |a[begin..end]|;
WH>}
WH>

WH>Без этого у меня квиксорт доказать не получается.

Поменяв местами первую и вторую строчку ассертов (как указано ниже), проверка проходит.
lemma TestMultiset(a : array<int>, begin : int, mid : int, end : int)
  requires a != null;
  requires 0 <= begin <= mid <= end <= a.Length;
{
  assert a[begin..mid] + a[mid..end] == a[begin..end];
  assert multiset(a[begin..mid]) + multiset(a[mid..end]) == multiset(a[begin..end]);
  assert |multiset(a[begin..mid])| + |multiset(a[mid..end])| == |multiset(a[begin..end])|;
  assert |a[begin..mid]| + |a[mid..end]| == |a[begin..end]|;
}


На всякий случай спрошу: в дафни важен порядок ассертов??
Best regards, Буравчик
Re[2]: Dafny, массивы и мультимножества
От: Буравчик Россия  
Дата: 15.05.16 23:04
Оценка:
Здравствуйте, Кодт, Вы писали:

К>А у тебя интервалы полуоткрытые или закрытые?
К>Для закрытых интервалов a[begin..mid] + a[mid..end] == a[begin..end] + a[mid], вообще-то.

Если я правильно понял, там slice, как в питоне.
Индексы как бы между элементами стоят.
Best regards, Буравчик
Re[2]: Dafny, массивы и мультимножества
От: WolfHound  
Дата: 16.05.16 07:59
Оценка:
Здравствуйте, Буравчик, Вы писали:

Б>Поменяв местами первую и вторую строчку ассертов (как указано ниже), проверка проходит.
Похоже, что дафна может доказать это условие
assert a[begin..mid] + a[mid..end] == a[begin..end];

и из его истинности вывести это
assert multiset(a[begin..mid]) + multiset(a[mid..end]) == multiset(a[begin..end]);

Но не может доказать второе условие без подсказок.

Б>На всякий случай спрошу: в дафни важен порядок ассертов??
Похоже, что да.
... << RSDN@Home 1.2.0 alpha 5 rev. 62>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Re[3]: Dafny, массивы и мультимножества
От: WolfHound  
Дата: 16.05.16 08:01
Оценка:
Здравствуйте, Буравчик, Вы писали:

Б>Если я правильно понял, там slice, как в питоне.
Б>Индексы как бы между элементами стоят.
Скорее нужно думать про индексы как про итераторы в STL.
... << RSDN@Home 1.2.0 alpha 5 rev. 62>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Re[4]: Dafny, массивы и мультимножества
От: Буравчик Россия  
Дата: 16.05.16 12:06
Оценка: +1
Здравствуйте, WolfHound, Вы писали:

WH>Здравствуйте, Буравчик, Вы писали:

Б>>Если я правильно понял, там slice, как в питоне.
Б>>Индексы как бы между элементами стоят.
WH>Скорее нужно думать про индексы как про итераторы в STL.

Мне все таки понятнее рассматривать так:



Так понятнее, почему весь массив это a[0..a.length]
И почему a[0..3] + a[3..6] не дублируют элемент 3
Best regards, Буравчик
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.