Вопросы по теме 'dafny'
Dafny - Методы вызова внутри операторов if?
Как следует из названия, я хотел бы вызвать метод, который изменяет некоторые переменные внутри оператора if другого метода, например:
method A
...
{
... // Modifies some variables
}
method B
...
{
...
if(statement){
A();...
918 просмотров
schedule
30.01.2023
Dafny: не найдено условий, вызывающих срабатывание сообщения об ошибке
У меня есть массив line , содержащий строку длины l , pat — это другой массив, содержащий строку длины p . Примечание. p и l не являются длиной массивов.
Цель состоит в том, чтобы увидеть, существует ли строка, содержащаяся в pat , в...
886 просмотров
schedule
21.12.2023
Можно ли использовать Dafny неинтерактивно, например, из программы на Python?
Я хотел бы узнать, проверяет ли конкретная программа Dafny. Dafny обычно используется для интерактивной разработки программ внутри Visual Studio IDE.
Однако мне нужно выполнить запрос неинтерактивным образом. В частности, мне нужно запросить...
99 просмотров
schedule
01.08.2023
Квантификатор Дафни не создается полезно при столкновении с тестовыми данными
Я пытаюсь создать предикат в dafny, который определяет, содержит ли массив символов дубликаты. В конечном итоге он должен проверять что-то вроде: для любых двух элементов в массиве, если значения theor равны, их индекс также должен быть равен....
80 просмотров
schedule
02.02.2023
суммирование списка чисел в dafny
Я использую dafny для доказательства инварианта суммирования списка чисел:
function sum (s: seq<int>, i: int) : int {
if |s| == 0 || i == 0 then 0
else s[0] + sum(s[1..], i - 1)
}
/*
code:
cnt = 0;
while i < |input|
cnt...
1215 просмотров
schedule
13.08.2022
Предикат Дафни ни истинен, ни ложен
Как может предикат Дафни быть ни истинным, ни ложным?
Этот:
predicate sorted(s: seq<int>)
{
forall j, k :: 0 <= j < k < |s| ==> s[j] <= s[k]
}
lemma SortedTest()
{
assert sorted([1, 3, 2]);
assert !sorted([1, 3,...
428 просмотров
schedule
06.06.2023
Модель Z3 для правильного метода Дафни
Может ли Z3 для правильного метода найти модель условия проверки метода?
Я думал, что нет, но вот пример, где метод правильный
однако проверка находит модель.
Это было с Dafny 1.9.7.
399 просмотров
schedule
19.05.2023
Как доказать количество Дафни ‹ размер
Сейчас я изучаю Дафни. Я полностью смущен леммой, и я не знаю, как ее использовать. Учебник не очень полезен. Что, если я хочу доказать count(a) <= |a| , как мне это сделать. Спасибо за помощь.
function count(a: seq<bool>): nat...
275 просмотров
schedule
27.12.2023
xbuild dafny на Linux ошибка CS0518
Я следовал инструкциям в документации по установке Dafny в Linux, но когда я использую xbuild dafny/Source/Dafny.sln , я получаю следующую трассировку:
reference:/usr/lib/mono/gac/System.Core/4.0.0.0__b77a5c561934e089/System.Core.dll /warn:4...
317 просмотров
schedule
29.04.2024
Контекст Dafny изменяет ошибку предложения
Мне очень трудно избавиться от последней ошибки в моей программе Dafny. Может ли кто-нибудь указать мне в правильном направлении? Вот код: http://rise4fun.com/Dafny/2FPo
Я получаю эту ошибку: присваивание может обновить элемент массива не в...
1763 просмотров
schedule
02.07.2023
Дафни: Почему я ввожу массив Дафни говорит, что это последовательность
Действительно ясно, что ввод представляет собой массив, но почему, когда он переходит к флагу [1..], он говорит, что флаг — это последовательность? Вот ссылка: http://rise4fun.com/Dafny/fUgu
620 просмотров
schedule
18.10.2023
(Dafny) Поиск в массиве - вариант цикла, ограниченный нулем?
Рассмотрим следующий код Dafny , который пытается найти элемент e внутри массива a :
method findE(a:array<int>, e:int, l:int, u:int) returns (result:bool)
requires a != null
requires 0 <= l <= u < a.Length
ensures...
504 просмотров
schedule
26.10.2022
Дафни отвергает простое постусловие
Ниже приведена первая попытка доказать различные простые теоремы, в данном случае о четности. Дафни /в. 1.9.9.40414/ проверяет, что добавление 2 к четному числу дает четное число, но не принимает ни одно из закомментированных условий.
function...
300 просмотров
schedule
26.11.2022
Инвариантный набор может варьироваться
Метод, который копирует отрицательные элементы массива целых чисел в другой массив, обладает тем свойством, что набор элементов в результате является подмножеством элементов в исходном массиве, который остается неизменным во время копирования....
295 просмотров
schedule
23.01.2024
Dafny Call может нарушать условие изменения контекста
Я пытаюсь проверить хэш-набор, но у меня возникла проблема с моим методом вставки.
Я не понимаю, почему я получаю сообщение об ошибке «вызов может нарушить условие изменения контекста», когда я раскомментирую вставки в main. Я считаю, что это...
835 просмотров
schedule
05.04.2023
Различные отсортированные предикаты должны быть эквивалентны в Dafny.
Согласно Автоматизация индукции с помощью SMT Solver на Dafny должно работать следующее:
ghost method AdjacentImpliesTransitive(s: seq<int>)
requires ∀ i • 1 ≤ i < |s| ==> s[i-1] ≤ s[i];
ensures ∀ i,j {:induction j} • 0 ≤ i < j...
142 просмотров
schedule
23.03.2023
Ограничения типа в Dafny: реализация Show для бинарного типа отношения
Я определил тип полиморфного бинарного отношения (класс) в Dafny:
class binRel<S,T>
Фактическая декларация:
class binRel<S(!new,==),T(!new,==)>.
Я хотел бы добавить новое ограничение типа: типы S и T должны реализовывать...
67 просмотров
schedule
08.02.2023
Покажи сумбурную ровность в Дафни
Вот код, который я пытаюсь доказать:
function rec_even(a: nat) : bool
requires a >= 0;
{
if a == 0 then true else
if a == 1 then false else
rec_even(a - 2)
}
method Even(key: int) returns (res: bool)
requires key...
191 просмотров
schedule
27.01.2023
Инвариант цикла Дафни, не поддерживаемый циклом
Моя задача — инициализировать матрицу 8x8 и убедиться, что все элементы внутри матрицы равны нулю. Я также должен использовать циклы while и инварианты циклов для реализации. Моя реализация выглядит так:
method initMatrix(a: array2<int>)...
2648 просмотров
schedule
03.11.2022
Функция Dafny, недопустимое логическое выражение в цикле while
Я новичок в Dafny и получаю некоторые ошибки, которые не могу понять.
в моей программе Dafny для insertionSort ( код находится здесь ), я не понимаю, почему я получаю invalid logical expression on В то время как цикл над переменной i ....
1180 просмотров
schedule
10.03.2024
