jml

    2热度

    1回答

    我们如何将JML应用于Java代码?我在“设计合同”中仍然是新手,但在如何将其应用到程序中却很失败。 http://jmlspecs.sourceforge.net/ 使用: OpenJML 的Netbeans 7.3 的Java SDK 1.7 我已经添加了OpenJML jar文件到NetBeans的类路径。我试过cofoga谷歌jml版本,你只需要 import com.google.jav

    1热度

    3回答

    我学习软件工程课程,在那里我看到了JML的使用。下面是一段代码示例: //@ requires f >= 0.0 public float sqrt(float f) { return f/2; } 它说正式的JML规范是可执行的! 我的问题是,当我们调用与F = -4这个sqrt函数,这段代码给出错误或抛出一个异常,或给予任何警告?我在我的电脑上试过它,它运行良好并打印出-2。

    1热度

    1回答

    我试图安装JML,是尝试各种Eclipse发行 但我收到此错误后成功运行Open JML: (使用Eclipse的Java的靛蓝SR2-win32)中 出现错误时我使用的菜单:JML>静态检查(ESC) 没有指定的证明是executeable - 使用-exec或定义openjml.prover 请提供一些帮助 Image Link

    1热度

    1回答

    即时尝试证明在我的集合中是否存在具有特定状态的对象。我的集合由一个名为getStatus()的方法组成。现在我想证明在这个集合中是否有一个具有给定状态的对象。 @ requires (\exists int i; 0 <= i && i < sizeLimit; orders[i].getStatus().equals(Status.New)); public Order getFirstOrd

    3热度

    1回答

    一个JML后置条件的一类方法可以包含调用另一个方法调用 例如,我有这个类: public class A { public int doA(x) { ... } public int doB(int x, int y) { ... } } 对于DOB的后置条件,我可以有:ensures doA(x) = doA(y)?

    3热度

    1回答

    我正在寻找一种用Java编写的能够读取JML的解析器。 基本上我希望解析器能够读取JML块并知道它属于哪个方法。 我一直在看OpenJML项目,但只是项目设置太多。

    0热度

    1回答

    有人能给出Java建模语言中的以下不变式的准确含义,指出它们之间的主要区别吗? 公共不变 抽象函数(私人不变) 表示不变(私人不变)

    0热度

    1回答

    当我尝试在http://jmlspecs.sourceforge.net/openjml-updatesite我收到以下错误安装从更新站点的openJML插件: An error occurred while collecting items to be installed session context was:(profile=epp.package.java, phase=org.ecli

    0热度

    1回答

    我需要JML的排序方法我尝试过Insertion Sort,但我不知道需要什么,并确保或维护我需要的东西。请帮忙。 我需要// @需要,// @确保和// @维护。 public class InsertionSort { void sort(int arr[]) { int n = arr.length; for (int i=1; i<n; ++i) {

    1热度

    1回答

    我正在使用JML来测试一些简单的类。我有类Interval.java,SequenceInterval.java和TestSequence.java,都在同一个包(默认包)中。当我尝试使用jmlc编译SequenceInterval时,它显示相同的错误: D:\work_java\VV_Lab1\src\JML>jmlc -Q SequenceInterval.java File "Sequen