Описание тега key-formal-verification
KeY - это формальный инструмент проверки программного обеспечения с открытым исходным кодом, в основном для дедуктивного доказательства правильности программного кода исходного кода Java.
1
ответ
Ключ изо всех сил пытается справиться с троичным оператором
Я играю с KeY ( https://www.key-project.org/) для учебного проекта. С одной стороны, я был счастлив, что KeY легко доказывает правильность следующего jml-аннотированного Java-кода. /*@ ensures ((\result == a) || (\result == b)); @ ensures ((\result …
04 дек '18 в 02:48
0
ответов
Формальная проверка ключа Java не может доказать цикл сброса массива
В настоящее время я пытаюсь понять немного формальной проверки с помощью инструмента Key для программ Java. Вот мой аннотированный Java-код: public class Test{ public int[] a; /*@ public normal_behavior @ ensures (\forall int x; 0<=x && x…
02 мар '19 в 13:37
0
ответов
Где светится инструмент проверки ключа?
Какие примеры кода демонстрируют силу KeY? подробности С таким количеством доступных инструментов Формального метода мне было интересно, где KeY лучше, чем его конкурент, и как? Некоторые читаемые примеры кода были бы весьма полезны для сравнения и …
15 окт '17 в 10:24
2
ответа
Почему эта проблема динамической логики KeY доказана, разумеется, увеличение java int 2147483647 на 1 должно быть -2147483648?
Ниже приведена запись для файла проблемы KeY Dynamic Logic (.key). Файл доказан, когда я использую доказательство теоремы KeY. Почему эта проблема динамической логики KeY доказана, разумеется, увеличение java int 2147483647 на 1 должно быть -2147483…
07 июл '20 в 21:08
1
ответ
Key Java JML proover передает этот алгоритм, который считывает определенный элемент массива, который вызывает исключение NullPointerException? вместо этого он должен потерпеть неудачу
Я пытаюсь лучше понять пределы проверки ключей для Java. Я придумал сценарий, в котором определенный элемент массива вызовет исключение нулевого указателя. Когда я пропускаю это через прувер, он проходит. Есть идеи, почему это так? Он должен заверши…
13 июл '20 в 22:22
1
ответ
Z3 отключить упрощение утверждений для доказательств
Есть ли способ отключить упрощение / переписывание утверждений в Z3 (версия 4.8.8)? В настоящее время я работаю над воспроизведением доказательств Z3 в KeY ( https://www.key-project.org). Однако, чтобы иметь возможность воспроизвести "утвержденное" …
17 окт '20 в 21:48
0
ответов
Формальная проверка ключа с помощью Xtext 2.25
Я работаю над проектом с формальной проверкой ключа на Java. Для этого я использую плагин Eclipse. Все работало нормально, когда у меня был Xtext версии 2.10. Однако по некоторым причинам я хочу обновиться до Xtext 2.25. К сожалению, сейчас я получа…
20 май '21 в 12:53
0
ответов
Ошибка при подключении решателя Z3 к KeY 2.8.0. в командной строке
Я новичок в KeY и пытаюсь все настроить, чтобы начать процедуры проверки. Для этого мне нужно включить SMT Solver: Z3. Я скачал файл Z3, но при заполнении пути к каталогу в командной строке в настройках Z3 в KeY получаю ошибку «null» (см. Снимок экр…
02 ноя '21 в 12:35
1
ответ
Невозможно доказать базовые функции, полагаясь только на реализации/встраивание
У меня есть курс этого класса. Я могу доказать переданный (int i) метод, когда использую контракт для getBar(), а не без него. Кроме того, контракт getBar() также доказан. Почему я не могу подтвердить передачу с помощью встраивания? Пробовал и Key 2…
08 мар '21 в 17:21