JML，不變量的精確定義

Question

有人能給出Java建模語言中的以下不變式的準確含義，指出它們之間的主要區別嗎？

• 公共不變
• 抽象函數（私人不變）
• 表示不變（私人不變）

Answer 1

能見度改性劑在JML reference manual解釋;關於不變量的可見性的簡短說明給出in this section。原理的見解是，

一個不變的訪問修飾符影響哪些成員，即哪些字段和（純）的方法，可以在它使用的，根據JML通常的可見性規則。

和

不變的訪問修飾符不影響的方法和構造，以保持和建立他們的義務。也就是說，無論不變量和方法的訪問修飾符如何，所有非輔助方法都應該保持不變式。例如，公共方法必須保留私有不變量以及公有變量。

也就是說，公共不變者可能會談論公共成員和私人成員，關於公共，受保護的，包裝可見和私人成員;所有的方法都必須建立所有的類不變量。

我真的不知道「抽象函數（私有不變量）」是什麼意思，在訪問修飾符中似乎沒有任何隱藏的語義含義，它們只是訪問修飾符而已，僅此而已。