Этот вопрос был первоначально размещен в Переполнении стека, и мне сказали разместить его здесь.

Я ассистент по обучению, готовлю задание для своих студентов, чтобы они могли изучать JML и проектировать по контракту. Я даю им 3 файла: RArray.refines-java (спецификация с пустыми утверждениями JML), RArray.java (класс, реализующий предыдущую спецификацию) и TestRArray.java (тестовый класс).

Для выполнения работы им нужно будет вычислить 3 команды:

  1. jmlc RArray.refines-java (компиляция спецификации и реализация)
  2. javac TestRArray.java (составление тестового класса)
  3. jmlrac TestRArray (проверка с помощью проверки утверждений во время выполнения jml)

Однако для этого им нужно установить JML на компьютеры в школе, где, очевидно, никто не имеет root-доступа. Сначала я попытался установить его, и, похоже, он не требует никакого root-доступа - я следовал этому французскому учебнику с этим zip-файлом.

Я попробовал на своем ноутбуке Ubuntu 14.04, он работал нормально, и я смог управлять некоторыми результатами для задания. Даже в школе, на Fedora, я могу без проблем устанавливать инструменты и добавлять их в PATH. Но в школе я сталкиваюсь с ошибкой при запуске jmlc RArray.refines-java .

Вот моя ошибка:

$ jmlc RArray.refines-java
parsing RArray.refines-java
parsing RArray1/RArray.java
typechecking RArray1/RArray.java
The .class file 'java/lang/CharSequence.class' appears to be malformed: Bad constant tag: 18
Fatal error - Unable to find a class for java/lang/CharSequence: error: Cannot find type "java.lang.CharSequence"

Я пытался выполнить поиск раньше, и, похоже, это может быть вопрос дубликатов CLASSPATH или чего-то в этих строках, но я не смог получить к нему доступ.

Я попытался также загрузить ZIP-файл снова, чтобы проверить, будет ли этот неправильный класс исправлен, но не повезло.

Я попытался запустить javac RArray.refines-java , и он компилируется, как и должно быть, поэтому это должно быть проблема с jml.

Вот результат java -version :

java version "1.8.0_66"
Java(TM) SE Runtime Environment (build 1.8.0_66-b17)
Java HotSpot(TM) 64-Bit Server VM (build 25.66-b17, mixed mode)

Вот результат jml -version :

Version: Common JML tools release 5.6_rc4 (Mar. 16, 2009)

У вас есть идеи, как это исправить? Надеюсь, мне не придется отказываться от всего.

|источник

1 ответ1

0

Насколько я знаю, JML работает только на Java 1.7

Попробуйте изменить ваш проект на Java 1.7 и посмотрите, работает ли он.Также проверьте, не является ли ваш компилятор версией выше поддерживаемой из JML.

Вот некоторая информация: [1]: http://jmlspecs.sourceforge.net/

@Редактировать

Я использую JML с Eclipse, и мне нужно выбрать Java 7, так как он будет автоматически переходить к 8. Также, если вы компилируете простой класс с терминалом, попробуйте следующую команду при его компиляции:$ javac -source 1.7 -target 1.7

|источник

Всё ещё ищете ответ? Посмотрите другие вопросы с метками .