Could someone give accurate meaning to the following invariants in Java Modelling Language pointing out the main difference between these?
- public invariant
- abstract function (private invariant)
- representation invariant (private invariant)
Could someone give accurate meaning to the following invariants in Java Modelling Language pointing out the main difference between these?
Copyright © 2021 Jogjafile Inc.
Visibility modifiers are explained in the JML reference manual; a short note on the visibility specifically of invariants is given in this section. The principle insight is that
and
That is, a public invariant may talk about public members and a private one about public, protected, package-visible and private members; and all methods have to establish all the class invariants.
I don't really know what you mean by "abstract function (private invariant)", there does not seem to be any hidden semantic meaning in the access modifiers, they're just access modifiers and nothing more.