關於工具的碎碎念

本文轉載自查看原文 2020-05-19 23:31 796

關於怎么用那些工具

下載說明，

（1）openjml+solver的zip：http://www.openjml.org/

（2） jmlunitng：http://insttech.secretninjaformalmethods.org/software/jmlunitng/

點擊里面那個 1.4 進行下載

正文第三段，單獨一行那個有個 1.4，點擊下載

1 solver

java -jar .\openjml.jar -exec C:\Users\73939\t\Solvers\z3-4.7.1.exe -esc C:\Users\73939\t\Group.java

這是我的文件樹，可以參考一下，我進入這個文件夾弄得

2 神奇的jmlunitng

弄好文件，依次輸入下面四條指令

java -jar jmlunitng.jar test/Group.java

javac -cp jmlunitng.jar test/*.java

java -jar openjml.jar -rac test/Group.java test/Person.java

java -cp jmlunitng.jar test.Group_JML_Test

文件樹同上，把代碼放到test里里面（我截圖兩個文件不參加編譯，只留着兩個副本備用的）

（我的是魔改版，去除了接口，更改了package的位置）

要是報加載找不到主類，就是你的文件package錯了

package test;

import java.math.BigInteger;
import java.util.ArrayList;

public class Person {
    public int id;
    public String name;
    public BigInteger character;
    public int age;
    public ArrayList<Person> acquaintance;
    public ArrayList<Integer> value;

    public Person(int id, String name, BigInteger character, int age) {
        this.id = id;
        this.name = name;
        this.character = character;
        this.age = age;
        acquaintance = new ArrayList<>();
        value = new ArrayList<>();
    }

    void addAcq(Person person) {
        acquaintance.add(person);
    }

    void addValue(int x) {
        value.add(x);
    }

    public int getId() {
        return id;
    }

    public String getName() {
        return name;
    }

    public BigInteger getCharacter() {
        return character;
    }

    public int getAge() {
        return age;
    }

    public boolean equals(Object obj) {
        if (obj != null && obj instanceof Person) {
            return (((Person) obj).getId() == id);
        } else {
            return false;
        }
    }

    public boolean isLinked(Person person) {
        if (person.getId() == id) {
            return true;
        }
        for (int i = 0; i < acquaintance.size(); i++) {
            if (acquaintance.get(i).getId() == person.getId()
                    || person.getId() == id) {
                return true;
            }
        }
        return false;
    }

    public int queryValue(Person person) {
        for (int i = 0; i < acquaintance.size(); i++) {
            if (acquaintance.get(i).getId() == person.getId()) {
                return value.get(i);
            }
        }

        return 0;
    }

    public int getAcquaintanceSum() {
        return acquaintance.size();
    }

    public Person getAcq(int x) {
        return acquaintance.get(x);
    }

    public int compareTo(Person p2) {
        return name.compareTo(p2.getName());
    }
}