JML无法找到类型

我正在使用JML来测试一些简单的类。我有类Interval.java，SequenceInterval.java和TestSequence.java，都在同一个包（默认包）中。当我尝试使用jmlc编译SequenceInterval时，它显示相同的错误：JML无法找到类型

D:\work_java\VV_Lab1\src\JML>jmlc -Q SequenceInterval.java 
File "SequenceInterval.java", line 22, character 42 error: Cannot find type "Interval" 
File "SequenceInterval.java", line 35, character 15 error: Cannot find type "Interval"

每一行我使用Interval类型的对象。这是我第一次使用ESCJava和JML，所以我是一个新手。我忘记了吗？我读了'模型导入'注释，但这不是我需要的，因为我在Java代码中使用了类Interval。那么，我该如何摆脱这个错误呢？这显然不是classpath的问题。 Tnx

来源

2011-03-11 joanna

+1使用ESCJava – MrSmith42 2013-02-23 17:12:17

您很可能需要将Interval.java也传递给jmlc。如果Interval.java尚未编译（以便在类路径中生成一个.class文件），ESC/Java2将不知道该类型。

来源

2011-03-30 00:45:18

JML无法找到类型

回答

相关问题