java - JML，不变量的准确定义

Question

有人可以对 Java 建模语言中的以下不变量给出准确的含义，指出它们之间的主要区别吗？

• 公共不变量
• 抽象函数（私有不变量）
• 表示不变量（私有不变量）

Answer 1

JML 参考手册中解释了可见性修饰符；本节给出了关于不变量的可见性的简短说明。主要观点是

根据 JML 通常的可见性规则，不变量的访问修饰符会影响其中可以使用哪些成员，即哪些字段和哪些（纯）方法。

和

不变量的访问修饰符不影响方法和构造函数维护和建立它们的义务。也就是说，无论不变量和方法的访问修饰符如何，所有非辅助方法都应保留不变量。例如，公共方法必须保留私有不变量以及公共不变量。

也就是说，公共不变量可以谈论公共成员，而私有不变量可以谈论公共、受保护、包可见和私有成员；并且所有方法都必须建立所有类不变量。

我真的不知道您所说的“抽象函数（私有不变量）”是什么意思，访问修饰符中似乎没有任何隐藏的语义含义，它们只是访问修饰符而已。