JML，不变量的精确定义

Question

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

• 公共不变量
• 抽象函数(私有不变量)
• 表示不变量(私有不变量)

Answer 1

可见性修饰符在JML参考手册中进行了解释；对于不变量的可见性，在本节中给出了一个简短的说明。主要的洞察力是

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

和

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

也就是说，公共不变量可以讨论公共成员，私有不变量涉及公共、保护、包-可见成员和私有成员；所有方法都必须建立所有的类不变量。

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