JML、不変式の正確な定義

Question

Javaモデリング言語の次の不変量に​​正確な意味を与えることができますか？

• 公共不変
• 抽象関数（プライベート不変）
• 表現不変（プライベート不変）

Answer 1

可視性改良剤はJML reference manualで説明されています。不変量の可視性に関する短い注釈はin this sectionと与えられている。不変の

アクセス修飾子は、フィールド及び（純粋）メソッドメンバー、すなわちに影響を与えるという原理洞察は、はJMLの通常の表示規則に従って、それに使用することができるされています。

と

不変量のアクセス修飾子を維持し、それらを確立するためのメソッドとコンストラクタの義務には影響を与えません。つまり、非ヘルパーメソッドはすべて、不変量とメソッドのアクセス修飾子に関係なく不変条件を保持することが期待されます。例えば、パブリックメソッドは、プライベートインバリアントおよびパブリックメソッドを保持する必要があります。

つまり、public invariantは、public、protected、package-visibleおよびprivateメンバーについてpublicメンバーとprivateメンバーについて話すことがあります。すべてのメソッドはすべてのクラス不変式を確立する必要があります。

"抽象関数（私的不変）"という言葉が本当に分かりませんが、アクセス修飾子に隠されたセマンティックな意味はないようです。