Вопросы по теме 'dafny'
Метод вставки Dafny, постусловие может не выполняться на этом пути возврата
У меня есть массив "line", в котором содержится строка длины "l", и массив "nl", в котором содержится строка длины "p". Примечание: «l» и «p» не обязательно должны быть длиной каждого соответствующего массива. Параметр «at» будет позицией, в которой...
1389 просмотров
schedule
21.05.2023
Почему использование new в функции Dafny дает ошибку?
Мне интересно, почему я получаю сообщение об ошибке для следующей программы:
class KV
{
var key : int;
var value : int;
constructor (k: int, v: int) modifies this
{
this.key := k;
this.value := v;
}
}
function foo () : KV
{...
336 просмотров
schedule
15.10.2022
Синтаксическая ошибка Dafny в функции
Я борюсь с синтаксисом дафни.
searchAndReplace получает три массива символов. Давайте представим, что line это [s][n][a][k][e] ; pat равно [n][a] , а dst равно [h][i] . Я хочу найти все вхождения pat в line и заменить его на dst ,...
1172 просмотров
schedule
02.05.2023
Странный(?) результат от БВД для программы Дафни
Когда я проверяю следующий фрагмент программы, в котором есть одна ошибка,
Я получаю следующий результат от BVD, который я не понимаю.
Меня озадачивает то, что второй инвариант, кажется, был проигнорирован при создании контрпримера....
84 просмотров
schedule
14.11.2022
(Dafny) Добавление элементов массива в другой - инвариант цикла
У меня есть функция sum , которая принимает два массива a и b в качестве входных данных и изменяет b таким образом, чтобы b[i] = a[0] + a[1] + ... + a[i] . Я написал эту функцию и хочу проверить ее с Дафни. Однако Дафни говорит мне, что мой...
971 просмотров
schedule
31.07.2022
попытка свидетеля null: результат операции может нарушить ограничение типа подмножества
Я написал класс, представляющий бинарное отношение в наборе S с двумя полями: этот набор S и второй набор пар значений, взятых из S. Класс определяет набор свойств отношений, таких как быть однозначным (т. е. быть функцией, как определено в предикате...
130 просмотров
schedule
17.11.2022
Карта проверки Дафни содержит значение
У меня есть карта типа map<int,char> в dafny, и я хочу посмотреть, содержит ли она какое-то значение.
Предполагая, что в dafny для этого еще нет синтаксиса, я начал создавать для него метод, но застрял. Мой код пока ниже:
method...
730 просмотров
schedule
24.09.2022
Дафни, замени индекс на значение в последовательностях
в руководстве по Dafny по адресу rise4fun s[i := v] определяется для замены индекса i на v в последовательности s . но использование этого всегда терпит неудачу с expected method call, found expression .
например, в приведенном ниже...
326 просмотров
schedule
06.03.2023
Дафни, вызов может нарушать условие изменения контекста
В моей программе (полная версия на rise4fun ) я хочу разделить массив, отсортировать каждый фрагмент и затем объедините их вместе.
Я решил использовать последовательности, потому что это упрощает нарезку и слияние. Затем, чтобы повторно...
664 просмотров
schedule
31.12.2022
Дафни, голландский флаг, инвариант цикла может не поддерживаться циклом
в приведенной ниже программе я создаю что-то вроде проблемы с голландским национальным флагом и следую той же логике, которая также представлена здесь программа сортирует массив из 0, 1 и 2 таким образом, что все 1 в начале, 0 в середине и 2 в...
611 просмотров
schedule
30.05.2023
Изменение параметров метода
Можно ли аннотировать параметры метода Дафни как изменяемые, не будучи объектами?
Моя цель - иметь возможность проверить
method testMethod(a:int, b:int) returns (res :int) {
res :=0;
a := (a - b);
assert a < (a-b);
}
Игнорируя тот...
168 просмотров
schedule
22.03.2023
Обновление карты другой картой в Дафни
Я хотел бы написать следующую функцию в Dafny, которая обновляет карту m1 всеми сопоставлениями из m2 , так что m2 переопределяет m1 :
function update_map<K, V>(m1: map<K, V>, m2: map<K, V>): map<K, V>
ensures...
350 просмотров
schedule
25.05.2023
Какой инвариант я пропустил в доказательстве BubbleSort?
Думаю, мне могут понадобиться дополнительные инварианты, чтобы убедить Дафни в том, что код работает. Я пробовал несколько, но не смог пройти.
method BubbleSort(arr: array<int>)
ensures forall k, k' :: 0 <= k < k' < arr.Length...
302 просмотров
schedule
25.05.2023
Утверждение о возвращаемом значении метода, включающего последовательности
Я новичок в Dafny, и мне интересно, почему нарушается утверждение непосредственно перед печатью в методе Main. Я пытаюсь найти самый правый индекс, куда следует вставить элемент, чтобы сохранить порядок в последовательности, которая в данном...
82 просмотров
schedule
14.12.2022
Предварительное условие Dafny для требования строки - это не только пробел
Я пытаюсь написать предварительное условие, чтобы строка содержала хотя бы один непробельный символ. Я написал следующее:
predicate AllWhiteSpaceChars(s: string) {
forall i :: 0 <= i < |s| ==> s[i] in {' ', '\n', /*'\f',*/ '\r',...
78 просмотров
schedule
01.08.2022
Инвариант цикла Дафни может не выполняться
Это простая задача разделения 0 и 1 в массиве. Я не могу понять, почему инвариант цикла не выполняется.
method rearrange(arr: array<int>, N: int) returns (front: int)
requires N == arr.Length
requires forall i :: 0 <= i <...
217 просмотров
schedule
21.08.2023
выражение свойств индуктивных типов данных в Dafny
Я определил тип данных сигма-алгебры в Dafny, как показано ниже:
datatype Alg = Empty | Complement(a: Alg) | Union(b: Alg, c: Alg) | Set(s: set<int>)
class test {
var S : set<int>
function eval(X: Alg) : set<int> //...
106 просмотров
schedule
16.01.2024
Что знает Дафни о петлях с разрывом?
I am used to loops
while Grd
invariant Inv
{ ..}
assert Inv && !Grd;
без перерыва Дафни знает, что Inv && ! Grd верно, но: Дафни не проверяет инвариант цикла после команды break; . Следовательно
method...
189 просмотров
schedule
04.06.2023
Dafny for-loop с оператором forall?
Я некоторое время работал в Dafny, и если мне приходилось использовать цикл for, я использовал оператор while , потому что я думал, что цикл for не существует в Dafny как встроенный.
Однако по этой ссылке ( Dafny, триггеры в назначении forall ) я...
240 просмотров
schedule
23.10.2022
Можно ли вызвать функцию внутри конструктора в dafny?
Я пытаюсь перевернуть логическое значение при создании экземпляра класса. Но я получаю следующую ошибку: в первом разделе тела конструктора (перед 'new;') 'this' можно использовать только для назначения его fieldsResolver .
Это действительно...
27 просмотров
schedule
27.03.2023
