JML找不到类型

Question

我正在使用JML测试一些简单的类。我有Interval.java、SequenceInterval.java和TestSequence.java类，它们都在同一个包(默认包)中。当我尝试使用jmlc编译SequenceInterval时，它显示了相同的错误：

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，所以我完全是个新手。我是不是忘了史密斯？我读到过“model import”注释，但这不是我需要的，因为我在Java代码中使用了类间隔。那么，我如何摆脱这个错误呢？这显然不是来自类路径的问题。Tnx

Answer 1

您很可能只需要将Interval.java传递给jmlc。如果Interval.java还没有编译(这样就在类路径上生成了一个.class文件)，ESC/jav2就不会知道它的类型。