Java契约下Natural类不变式实现问询：异常控制与溢出拦截

现有代码的问题 #

1. noUnexpectedExceptions() 作为不变式逻辑不成立：不变式是用来验证对象状态的合法性，而非检查方法的异常抛出行为。这个方法既无法约束方法只抛出指定异常，也不属于对象状态的范畴。
2. increment() 和 decrement() 未做边界检查：执行data++当data已是Integer.MAX_VALUE时会溢出为负数，data--当data为0时会变成-1，直接违反data >=0和data <= Integer.MAX_VALUE的不变式，且没有抛出要求的异常。

修正后的实现 #

@Invariant({
    "data >= 0",
    "data <= Integer.MAX_VALUE"
})
public class Natural implements Comparable<Natural> {
    private int data;

    // 构造方法初始化合法值
    public Natural() {
        this.data = 0;
    }

    public Natural(int initialValue) {
        if (initialValue < 0 || initialValue > Integer.MAX_VALUE) {
            throw new PreconditionError("初始值必须在0到Integer.MAX_VALUE之间");
        }
        this.data = initialValue;
    }

    public void increment() {
        if (data == Integer.MAX_VALUE) {
            throw new PreconditionError("increment操作会导致溢出，当前值已达最大值");
        }
        data++;
        // 可选：手动验证不变式，若框架未自动触发
        if (data > Integer.MAX_VALUE || data < 0) {
            throw new InvariantError("违反Natural类状态不变式");
        }
    }

    public void decrement() {
        if (data == 0) {
            throw new PreconditionError("decrement操作会导致下溢，当前值已是最小值");
        }
        data--;
        // 可选：手动验证不变式
        if (data > Integer.MAX_VALUE || data < 0) {
            throw new InvariantError("违反Natural类状态不变式");
        }
    }

    @Override
    public int compareTo(Natural o) {
        return Integer.compare(this.data, o.data);
    }

    public int getData() {
        return data;
    }
}

关键说明 #

1. 不变式的正确范围：只保留data的数值范围约束，这是Natural对象必须始终维持的核心状态——从创建到销毁，data必须在[0, Integer.MAX_VALUE]之间。
2. 溢出/下溢的阻止：
   • 在increment()前检查data是否已达最大值，若达到则抛出PreconditionError（属于操作前的前置条件不满足）。
   • 在decrement()前检查data是否为0，若为0则抛出PreconditionError。
   • 操作后可手动验证不变式，若状态非法则抛出InvariantError，确保任何情况下都不会违反状态约束。
3. 异常类型的约束：
   • 所有可能触发的异常仅为PreconditionError或InvariantError：构造方法、增减操作中只抛出PreconditionError；状态验证失败时抛出InvariantError。
   • 杜绝其他类型异常：所有方法逻辑中均不引入可能抛出其他异常的操作，确保异常类型符合要求。

内容的提问来源于stack exchange，提问作者Hamid Ayub