JML, точное определение для инвариантов
Может ли кто-то дать точное значение следующим инвариантам в языке моделирования Java, указывая на основное различие между ними?
- публичный инвариант
- абстрактная функция (частный инвариант)
- инвариант представления (частный инвариант)
1 ответ
Модификаторы видимости объяснены в справочном руководстве JML; в этом разделе дается короткое примечание о видимости конкретно инвариантов. Принцип понимания заключается в том, что
Модификатор доступа инварианта влияет на то, какие члены, т.е. какие поля и какие (чистые) методы, могут использоваться в нем, согласно обычным правилам видимости JML.
а также
Модификаторы доступа инвариантов не влияют на обязательства методов и конструкторов поддерживать и устанавливать их. То есть все не вспомогательные методы должны сохранять инварианты независимо от модификаторов доступа инвариантов и методов. Например, публичный метод должен сохранять как частные, так и инварианты.
То есть публичный инвариант может говорить об открытых членах, а частный - об открытых, защищенных, видимых в пакете и закрытых членах; и все методы должны устанавливать все инварианты классов.
Я действительно не знаю, что вы подразумеваете под "абстрактной функцией (частным инвариантом)", в модификаторах доступа, кажется, нет никакого скрытого семантического значения, это просто модификаторы доступа и ничего более.