Описание тега jml
Java Modeling Language (jml) - язык спецификаций для Java
1
ответ
Проверка контрактов в Maven Build
Я работаю над базой кода Java в IJ и в настоящее время собираюсь с Maven. Я хотел бы дополнить некоторый код некоторыми формами контрактов, которые будут собраны в сборке Maven. До сих пор мне не удавалось найти такую возможность с полки: OpenJML,…
29 май '18 в 15:23
1
ответ
Что означает "присваиваемый a, a[*];" имею в виду?
Я недавно прочитал следующий код JML в старом экзамене: Class L { /*@non_null*/ int[] a; /*@ public normal_behaviour @ requires !(\exists int i; 0 <= i && i < a.length; a[i] == d); @ ensures a.length == \old(a.length) + 1; @ ensures a[…
04 мар '15 в 05:18
1
ответ
Попытка запустить Open JML в Eclipse
Я пытаюсь установить JML и добился успеха после попытки различных дистрибутивов затмения, но я получаю эту ошибку: (используя eclipse-java-indigo-SR2-win32) ошибка появляется, когда я использую меню: JML > Статическая проверка (ESC) Исполняемый файл…
29 мар '14 в 06:42
1
ответ
Постусловие JML содержит вызов метода класса
Может ли постусловие JML для метода класса содержать вызов другого метода Например, у меня есть этот класс: public class A { public int doA(x) { ... } public int doB(int x, int y) { ... } } Для постусловия doB я могу иметь: ensures doA(x) = doA(y)?
28 ноя '12 в 10:32
1
ответ
JML: Как указать требование массива с полумесяцами?
Я хочу сделать это в JML: //@ requires (\forall int i : array[i] < array[i+1]) void calculatesDistances(int[] array){ .. } Я не мог заставить это работать, видел много примеров в спецификациях JML, но не мог найти способ, как это сделать. Итак, к…
15 окт '10 в 22:17
2
ответа
OpenJML с дженериками?
У меня есть класс Edge.java, Когда я запускаю его через OpenJML, это происходит: error: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can. Reason: com.sun.tools.javac.code.Symbol$TypeSymb…
06 май '14 в 08:47
2
ответа
Установка JML в Eclipse
Я использую Eclipse для программирования на Java. Я попытался установить с этого сайта, хотя Eclipse Updater, но, хотя он не выдавал никакой ошибки, я не вижу меню, которое, как они говорят, мне следует. Может быть, я должен сначала установить что-т…
11 мар '10 в 17:49
2
ответа
Android: библиотека JML для MSN не работает на Android 2.1?
Мне удалось подключиться к MSN через библиотеку JML на Android, добавив класс getpropertyaction в моем проекте. На андроиде 2.2 работает просто отлично, я могу залогиниться, получить контакты, отправлять и получать сообщения и прочее.. На Android 2.…
04 фев '11 в 10:16
1
ответ
Метод сортировки Java в JML
Мне нужен метод сортировки для JML. Я пробовал сортировку вставками, но я не знаю, что требует и обеспечивает или поддерживает то, что мне нужно. Пожалуйста помоги. Мне нужно //@ требует, //@ обеспечивает и //@ поддерживает. public class InsertionSo…
27 дек '17 в 14:48
1
ответ
Как мы применяем JML (openJML) к коду Java?
Как мы применяем JML к коду Java? Я все еще новичок в дизайне по контрактам и совершенно не знаю, как применить его в программе. http://jmlspecs.sourceforge.net/ С помощью: OpenJML Netbeans 7.3 Java SDK 1.7 Я уже добавил файлы jar OpenJML в путь к к…
28 авг '13 в 14:50
1
ответ
Альтернативы JML
Я ищу альтернативные варианты языков спецификации для Java, такие как JML. Кто-нибудь знает кого-нибудь? Благодарю.
08 янв '11 в 12:39
1
ответ
Простой парсер для JML
Я ищу парсер, написанный на Java, способный читать JML. По сути, я бы хотел, чтобы синтаксический анализатор мог читать блок JML и знать, к какому методу он принадлежит. Я смотрел на проект OpenJML, но просто настройки проекта слишком много.
13 апр '11 в 16:45
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
1
ответ
Как настроить мою среду для ESC/Java2 в Windows и собрать / запустить с ESC/Java2?
Как настроить среду выполнения для ESC/Java2 в WindowsXP? И более того, как мне создавать и запускать в WindowsXP проекты с ESC/Java2. Трудно сказать по их спецификациям /readme и документации, особенно учитывая тот факт, что они, похоже, больше гов…
16 окт '08 в 20:40
2
ответа
Почему JML не реализован как аннотации в Java?
В отличие от кодовых контрактов в C#, в JML кодовые контракты - это просто текст, который используется в виде комментариев в заголовке метода. Разве не было бы лучше, чтобы они выставлялись как аннотации? Таким образом, даже при компиляции информаци…
18 мар '10 в 21:02
1
ответ
JML, точное определение для инвариантов
Может ли кто-то дать точное значение следующим инвариантам в языке моделирования Java, указывая на основное различие между ними? публичный инвариант абстрактная функция (частный инвариант) инвариант представления (частный инвариант)
19 июл '17 в 17:51
0
ответов
JML не может поймать нарушенное предусловие
В моем классе Test у меня есть массив из пяти int с именем a и метод addOne(int index), который добавляет один к выбранной ячейке. Я написал в JML простое предварительное условие для управления индексом, переданным методу. Затем я пытаюсь нарушить э…
08 июл '15 в 10:59
1
ответ
Что является постусловием для метода java PriorityQueue.remove(Object)?
Я смотрю на создание JML-спецификаций для метода java.util.PriorityQueue.remove(Object object). До сих пор я думал о следующем предварительном условии: //@ requires object != null; //@ requires this.size() > 0; Я сейчас пытаюсь выяснить постуслов…
08 дек '15 в 01:32
3
ответа
Исполняемый язык моделирования Java?
Я изучаю курс разработки программного обеспечения, и там я увидел использование JML. Вот пример кода: //@ requires f >= 0.0 public float sqrt(float f) { return f/2; } Это говорит о том, что формальные спецификации JML являются исполняемыми! Мой в…
28 май '13 в 21:27
1
ответ
JML не нулевые варианты?
У меня есть вопросы JML. в чем разница между /*@ invariant array_ != null; */ и объявив его как protected /*@ non_null */ Object[] array_; относительно элементов array_? Какое свойство имеет для них в каждом случае? Заранее спасибо.
05 дек '10 в 15:10