Описание тега openjml
OpenJML is a tool for working with logical annotations in Java programs.
1
ответ
Проверка контрактов в Maven Build
Я работаю над базой кода Java в IJ и в настоящее время собираюсь с Maven. Я хотел бы дополнить некоторый код некоторыми формами контрактов, которые будут собраны в сборке Maven. До сих пор мне не удавалось найти такую возможность с полки: OpenJML,…
29 май '18 в 15:23
2
ответа
Рассуждения о реалах
Я экспериментирую с OpenJML в сочетании с Z3 и пытаюсь double или же float ценности: class Test { //@ requires b > 0; void a(double b) { } void b() { a(2.4); } } Я уже выяснил, использует OpenJML AUFLIA как логика по умолчанию, которая не поддерж…
14 июл '15 в 17:42
1
ответ
OpenJML/ Джесси для Android
Я пытаюсь статически проверить Java мой код. Единственная проблема заключается в том, что он использует Android SDK и OpenJML не может идентифицировать классы Android. Например, это часть журналов, которые я получаю: app/src/main/java/rup/ino/catorn…
17 дек '18 в 16:54
1
ответ
Как убрать пробелы после комментариев в автоформатировании Eclipse?
Я использую плагин OpenJML для своего проекта, но автоматическое форматирование Eclipse портит мой код JML. JML написан после //@ условное обозначение. //@ requires password != null; //@ ensures !isActive() && getPassword().testWord(password…
01 дек '17 в 09:25
1
ответ
Итерация по матрице с openJML
У меня есть класс с матрицей, инициализированной со всеми 0 и 1 в определенной позиции: public class MatrixTest { /*@ spec_public @*/ int[][] griglia; //@requires true; //@ensures griglia[2][3] == 1; public MatrixTest() { griglia = new int[6][6]; fo…
29 май '16 в 14:42
0
ответов
Ошибка "Поиск внутренних спецификаций" с плагином OpenJML в Eclipse
У меня OpenJML установлен как Eclipse Plugin (установить сайт http://jmlspecs.sourceforge.net/openjml-updatesite ) в Eclipse Photon, мой проект (но не сам Eclipse) использует OpenJDK 1.8 Тем не менее я получаю эту ошибку, и я не могу найти, почему: …
12 апр '19 в 10:20
1
ответ
Используйте OpenJML в проекте Eclipse, который использует JDK, отличный от OpenJDK 1.8
OpenJML доступен как плагин Eclipse (сайт установки http://jmlspecs.sourceforge.net/openjml-updatesite) и, похоже, в Eclipse Photon устанавливается нормально. Но в документах говорится, что он должен работать только на OpenJDK 1.8 и не может быть др…
12 апр '19 в 09:43
0
ответов
Ошибки при запуске OpenJML с двумя классами
Я проверил оба следующих фрагмента кода с помощью OpenJML: public class Customer { /*@ public invariant this.customerID != 0; */ /*@ public invariant this.customerID >= -1; */ /*@ spec_public */ private int customerID; /*@ @ public normal_behavio…
10 июн '20 в 00:53
1
ответ
Как я могу увидеть сообщения об ошибках OpenJML?
Когда я запускаю свой код с тестом OpenJML в eclipse. Я получаю этот вывод...... Пропуск длительных тестов Обнаружено 5 классов системных спецификаций для esc-тестирования JRE версии 1.8.0_202 5 классов системных спецификаций найдено для rac-тестиро…
09 дек '19 в 17:39
1
ответ
JML - OpenJML с расширенной статической проверкой - пример массива
Я только начал использовать OpenJML, вот мой код и предупреждение JML: Код: //@ requires myArray != null ; //@ ensures myArray == \old(myArray) ; //@ signals ( MathLibException ) myArray.size() == 1 ; public ArrayList<Integer> ExceptionTest1 (…
10 июл '20 в 11:18
1
ответ
Key Java JML proover передает этот алгоритм, который считывает определенный элемент массива, который вызывает исключение NullPointerException? вместо этого он должен потерпеть неудачу
Я пытаюсь лучше понять пределы проверки ключей для Java. Я придумал сценарий, в котором определенный элемент массива вызовет исключение нулевого указателя. Когда я пропускаю это через прувер, он проходит. Есть идеи, почему это так? Он должен заверши…
13 июл '20 в 22:22
0
ответов
Как написать спецификацию OpenJML?
Мне нужно реализовать спецификацию для пары методов моей домашней работы. Я провел небольшое исследование в Интернете и прочитал документацию, и все, что я обнаружил, это то, что в основном речь идет о добавлении предварительных и пост-условий. Но м…
08 июн '20 в 16:00
1
ответ
Правильный способ установки JML
Я попытался установить язык моделирования Java (JML), но что-то пошло не так. Я использую Eclipse IDE, windows 10. Я открыл Eclipse -> Help -> Install New Software, а затем установил с помощью этого Затем я перезапустил Eclipse, и в верхней строке м…
25 окт '20 в 20:45
0
ответов
Проблема алгоритма с двумя суммами встречает openjml: основные вопросы
Я пытаюсь разобраться в JML через OpenJML и подумал, что очень классным примером может быть двузначный вопрос о каноническом алгоритме: https://leetcode.com/problems/two-sum Каноническое решение - использовать хеш-таблицу для запоминания видимых эле…
21 окт '20 в 03:28
1
ответ
Почему OpenJML не может доказать утверждение в цикле for?
У меня есть следующий фрагмент кода: //@ requires dest != null; //@ requires srcOff >= 0; //@ requires destOff >= 0; //@ requires length >= 0; //@ requires srcOff < src.length; //@ requires destOff < dest.length; //@ requires srcOff +…
14 дек '20 в 15:13
0
ответов
Постусловие OpenJML (и инвариант цикла) содержит вызов метода класса
Я хотел бы вызвать метод класса в постусловии (и инварианте цикла) другого метода. Наиболее подходящей вещью, которую я нашел, был этот пост в StackOverflow. Я попытался открыть предоставленную там ссылку ( http://www.ibm.com/developerworks/java/lib…
18 фев '22 в 21:30
1
ответ
JML удалить предупреждение после вызова функции
Мне дали задание, в котором я должен удалить все предупреждения, созданные JML. Если я вызываю метод внутри конструктора, my и больше не проверяются, несмотря на добавление того же ограничения для вызываемой функции. Меня просят использовать только …
13 дек '20 в 09:52
0
ответов
Предупреждение OpenJML в Java
Я новичок в предупреждениях JML и пытаюсь удалить все предупреждения для этой функции: //@ requires input <= Integer.MAX_VALUE; //@ requires input >= 0; //@ ensures \result >= 0; //@ signals (Exception) input >= Integer.MAX_VALUE; //@ en…
08 май '22 в 17:07
0
ответов
Ошибка ввода JML: здесь необходимо состояние памяти (\at отсутствует?)
Я пытался исправить ошибку в своей программе JML, но мне это не удалось. Это опечатка, которая ссылается на файл «Practi.jc», о том, где он находится, я понятия не имею. //@+CheckArithOverflow=no /*@ axiomatic Addition{ @logic integer sum(int [] x, …
26 май '23 в 10:34