Esta questão foi originalmente publicada em Stack Overflow , e me disseram para postar aqui em vez disso.
Eu sou um Assistente de Ensino preparando uma tarefa para meus alunos, para que eles aprendam sobre o JML e o design por contrato. Eu dou 3 arquivos para eles: RArray.refines-java (uma especificação com asserções JML em branco), RArray.java (a classe que implementa a especificação anterior) e TestRArray.java (uma classe de teste).
Para realizar o trabalho, eles terão que computar 3 comandos:
jmlc RArray.refines-java (compilação da especificação e implementação) javac TestRArray.java (compilação da classe de teste) jmlrac TestRArray (verificação com verificador de asserção de tempo de execução jml) Para fazer isso, no entanto, eles precisam instalar o JML nos computadores da escola, onde obviamente ninguém tem acesso root. Eu tentei instalá-lo primeiro, e parece que não requer nenhum acesso root - eu segui este tutorial em francês , com este arquivo zip .
Eu tentei no meu laptop Ubuntu 14.04, funcionou muito bem e eu fui capaz de gerenciar alguns resultados para a atribuição. Mesmo na escola, no Fedora, posso instalar as ferramentas sem reclamar e adicioná-las ao PATH. Mas, na escola, encontro um erro quando corro
jmlc RArray.refines-java .
Aqui está o meu erro:
$ 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"
Eu tentei pesquisar antes, e parece que pode ser uma questão de CLASSPATHs duplicados, ou algo nessas linhas, mas não consegui acessá-lo.
Eu também tentei baixar o arquivo ZIP novamente, para verificar se essa classe malformada seria corrigida, mas sem sorte.
Eu tentei executar javac RArray.refines-java e ele compila como deveria, portanto, deve ser um problema de jml.
Aqui está o resultado de 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)
Aqui está o resultado de jml -version :
Version: Common JML tools release 5.6_rc4 (Mar. 16, 2009)
Você tem alguma ideia de como consertar isso? Espero não ter que descartar tudo.
Até onde eu sei, o JML só funciona no java 1.7
Tente alterar seu projeto para o java 1.7 e veja se ele funciona. Também verifique se o seu compilador não é uma versão acima do suportado pelo JML.
Aqui estão algumas informações: [1]: link
@Editar
Eu uso o JML com o Eclipse e preciso escolher o Java 7, pois ele iria automaticamente para o 8. Além disso, se você estiver compilando uma classe simples com o terminal, tente o seguinte comando ao compilá-lo: $ javac -source 1.7 -target 1.7