Описание тега boogie
Boogie - это промежуточный язык проверки, созданный в Microsoft Research и предназначенный в качестве слоя для создания программных верификаторов для других языков.
0
ответов
Моделирование вектора / массива фиксированного размера в Boogie
Я пытаюсь моделировать векторы фиксированной длины в буги. Каждый вектор с разным размером должен быть другого типа. Я попробовал два подхода, но у обоих есть особая проблема. Подход 1: Тип псевдонимов Определите псевдоним типа и некоторые аксиомы, …
26 июл '18 в 08:35
0
ответов
Логическая ошибка или ошибка Буги? Квантификаторы: существует из-за
Я работаю с языком верификации Boogie, где у меня есть следующий пример, который дает результат, который мне противоречит. // Defining a function and giving it a meaning through axiomatization. function EqualsInt(x: int, y: int) : bool; axiom (foral…
03 авг '18 в 13:09
1
ответ
Могу ли я найти пример счетчика нечестных, если я использую другой буг-бенд для проверки переведенных файлов bpl Dafny?
Как упоминалось в вики на Dafny GitHub, когда Dafny не может доказать утверждение в программе, это может быть связано либо с неверной моей программой, либо с неполностью Dafny. Но я подумал, что контрпример от Дафни поддельный после того, как я попы…
12 сен '18 в 19:25
1
ответ
Как читать дафны контрпримеры
Я хотел бы понять контрпримеры, произведенные Дафни. Я использую следующий код в качестве примера: function update_map<K(!new), V>(m1: map<K, V>, m2: map<K, V>): map<K, V> ensures (forall k :: k in m1 || k in m2 ==> k in u…
03 окт '18 в 01:54
1
ответ
Что такое триггеры в Дафни / Буги?
Я бездельничал в Дафни, не понимая триггеров. Возможно, в результате программы, которые я пишу, кажутся трудным временем для верификатора. Иногда я трачу кучу времени, возясь с доказательством, пытаясь убедить Дафни / Буги в том, что оно действитель…
03 июн '18 в 16:44
0
ответов
Как написать инвариант для 2 цикла в буги
Я обнаружил, что трудно написать инвариант для некоторого цикла В буги, даже цикла с простой формой, как показано ниже. Код буги хочет поместить двумерный массив src в одномерный массив des, но инварианты трудно описать это намерение. procedure f() …
13 авг '19 в 06:51
1
ответ
Каковы источники ненадежности доказательств Дафни?
Я иногда (не часто, но достаточно часто) вижу, что доказательство будет работать в Dafny, а затем что-то, что кажется неуместным, изменится (например, имена переменных, определение функции, не имеющее отношения к доказательству и т. Д.) и доказатель…
20 авг '20 в 04:23
1
ответ
Инварианты и old() в буги-вуги
Я проверяю следующий фрагмент кода с помощью буги-вуги: var v: int; procedure main() modifies v; { v := 0; while(true) invariant v > old(v) || v == 0; { v := v+1; } } И вывод: main2.bpl(10,9): Error: This loop invariant might not be maintained by…
16 фев '21 в 14:56
0
ответов
Влияет ли random_seed на начальное состояние параметров в реализации?
Я заинтересован в использовании атрибута random_seed для разнообразия значений, возвращаемых контрпримером z3. Например, эта реализация имеет 3 параметра разных типов. implementation {:random_seed N} Impl$$_module.__default.isOddLength(i#0: int, j#0…
25 май '22 в 22:11
0
ответов
Векторы и последовательности в буги-вуги
Просматривая тесты, поставляемые с Boogie, я заметил, что существует два типа коллекций:Seq TиVec T. Примеры: type {:builtin "Seq"} Seq _; function {:builtin "seq.empty"} empty(): Seq int; function {:builtin "seq.len"} len(a: Seq int): int; function…
08 июн '22 в 21:55