static_invariant_for

[davidcok]

I notice in a list of features that KeY uses static_invariant_for to, I presume, get a static invariant of a class.

OpenJML just uses \invariant_for() as in \invariant_for(Integer) or \invariant_for(java.lang.Integer) to get static invariants. Would that be an OK simplification/unifiication of syntax for KeY?

Also, in KeY, does \invariant_for(o) for some expression o

• yield the invariant for the dynamic or static type of o?
• include the static invariant of o?

[mattulbrich]

in KeY:

\invariant_for yields the dynamic invariant. This is quite an important aspect of dynamic frame abstraction.

(Of course, when receiving objects, one can often only unwrap the invariants of the guaranteed static type.)

\invariant_for does not include the static invariant.

[leavens]

Hi Mattias, David, and all,

Let us refer to a class-level invariant that can mention static fields as a "static invariant" (sometimes this is called a class invariant, but that may be a confusing term), and invariants that only mention instance fields as an "object invariant".

So, the semantics of \invariant_for(E) returns the object invariant of the static type of E, if I understand that correctly. Is there a way to specify the type directly, such as \invariant_for(E.class) (to get the object invariant for the E's dynamic type)?

Then it makes sense to have something like \static_invariant_for(T) to return the static invariant for the type T.

    Regards,

    Gary T. Leavens
    329 L3Harris Center
    Computer Science, University of Central Florida
    4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
    http://www.cs.ucf.edu/~leavens phone: +1-407-823-4758
    ***@***.******@***.***>

[davidcok]

Gary.

• A (static) class invariant can mention only static fields
• An instance invariant can mention both static and instance names

For an expression e, \invariant_for(e) returns the invariant for the dynamic type of e, according to KeY, though probably the static type of e according to current JML (and OpenJML)

One can write a class directly as just the class name (Integer) or as an expression (Integer.class) or even in JML as \type(T) so as to keep a non-erased type (.class does erasure)

OpenJML users \invariant_for(T) to get the static invariant of the class T OpenJML could use \invariant_for(T.class) but that seems unnessarily verbose

KeY uses static_invariant_for but I’m not sure what the argument is.

• David

On Dec 13, 2021, at 11:06 AM, Gary T. Leavens @.***> wrote:

Hi Mattias, David, and all,

Let us refer to a class-level invariant that can mention static fields as a "static invariant" (sometimes this is called a class invariant, but that may be a confusing term), and invariants that only mention instance fields as an "object invariant".

So, the semantics of \invariant_for(E) returns the object invariant of the static type of E, if I understand that correctly. Is there a way to specify the type directly, such as \invariant_for(E.class) (to get the object invariant for the E's dynamic type)?

Then it makes sense to have something like \static_invariant_for(T) to return the static invariant for the type T.

[leavens]

Hi David,

Thanks for the correction about the meaning and restrictions on static invariants and for the other information.

    Regards,

    Gary T. Leavens
    329 L3Harris Center
    Computer Science, University of Central Florida
    4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
    http://www.cs.ucf.edu/~leavens phone: +1-407-823-4758
    ***@***.******@***.***>

[mattulbrich]

\static_invariant_for(java.lang.Integer) refers to the static invariant for the class in KeY. So the argument is a (qualified) class name.

I think \invariant_for(Integer.class) would also be fine I think.

I have an example why dynamic invariant is better, will post that later.

[davidcok]

Why not just \invariant_for(java.lang.Integer)

On Dec 13, 2021, at 11:19 AM, Mattias Ulbrich @.***> wrote:

\static_invariant_for(java.lang.Integer) refers to the static invariant for the class in KeY. So the argument is a (qualified) class name.

I think \invariant_for(Integer.class) would also be fine I think.

[leavens]

Hi David, Mattias, and all,

I think it would be best if the operator distinguished whether the static (class) invariant or the dynamic (object) invariant is needed, as to me that seems clearer and avoids the need for the implementation to perform overload resolution on operators.

    Regards,

    Gary T. Leavens
    329 L3Harris Center
    Computer Science, University of Central Florida
    4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
    http://www.cs.ucf.edu/~leavens phone: +1-407-823-4758
    ***@***.******@***.***>

[davidcok]

On Dec 13, 2021, at 1:34 PM, Gary T. Leavens @.***> wrote:

Hi David, Mattias, and all,

I think it would be best if the operator distinguished whether the static (class) invariant or the dynamic (object) invariant is needed, as to me that seems clearer and avoids the need for the implementation to perform overload resolution on operators.

OK I’ll concede on adding static_invariant_for to JML. — our examples have used a type name — is an expression allowed? — if so, does static_invariant_for(e) return the static invariant of the static or dynamic type of e? — and, as JML has \TYPE values, do we allow \TYPE t = typeof(x) or \TYPE t = \type(Integer) and then static_invariant_for(t) — which would then be using the value of t rather than the type of t as in the previous question

Remember that MU said that \invariant_for(e) does not include any static invariants of the type of e

[leavens]

If \static_invariant_for(T) is going to refer to a type, then I would suggest that we make it name a type directly, without using an expression. Adding a layer of evaluation would just complicate its usage in tools.

[davidcok]

OK. I think are we agreed on the simple approach:?

\invariant_for(o) takes an object reference and returns the instance invariant for the dynamic type of the given object (conjunction of relevant invariant clauses for the visibility of the context)

\static_invariant_for(T) takes a type name and returns the conjunction of the visible static (class) invariants for just that type (no super or sub types or interfaces).

[If you are concerned about the visibility part, let's take that up as a separate topic.]

[mattulbrich]

Let us keep the visibility part of this here. It is interesting, however.

We very often have to specify:

//@ public invariant next != null ==> \invariant_for(next);

Can we make this

//@ public invariant \invariant_for(next);

by saying that \invariant_for(null) := true.

Would really produce shorter specifications, and is easily described "returns the invariant of the argument if that is not null, and true otherwise".

[leavens]

Yes, to me that makes sense since non-null is the default semantics for JML.

[mattulbrich]

Yes, to me that makes sense since non-null is the default semantics for JML.

But for linked data structures, one oftentimes has nullable next pointers to allow for structures to end. This null check is syntactic noise then.

[davidcok]

I'm OK with that. The only reasonable alternative is to say that \invariant_for(null) is not well-defined.

But on the visibility. Do both \invariant_for and \static_invariantfor collect the conjunction of all the invariants (static, respectively) or all the invariants visible at the point of the (static)invariant_for? I think I'm in favor of ignoring visibility here.

[mattulbrich]

I do have an opinion on this, but I'd say we'd open a followup item to not lose the results obtained here.

[davidcok]

Visibility discussion moved to #32. Closing this issue with this resolution:

\invariant_for(o) takes an object reference and returns the instance invariant for the dynamic type of the given object (conjunction of relevant invariant clauses, including invariants of its super types)

\invariant_for(null) is true

\static_invariant_for(T) takes a type name and returns the conjunction of the static (class) invariants for just that type (no super or sub types or interfaces).

[leavens]

I'm fine with most of this, but I think it's a mistake for \invariant_for(o) to be the instance invariant of the dynamic type of o. For static verification, I think it will need to be the instance invariant of the static type of o.

[mattulbrich]

I have claim to have a compelling example why this should be the dynamic type in this comment on #32

[davidcok]

As I'm writing this up, a couple questions:

1) For static_invariant_for, I expect that the argument should be a fully parameterized type?

2) For static_invariant_for and invariant_for, does the order of conjoining invariants matter -- that is do we need to require textual order? That is, may invariants depend on textually previous invariants to be well-defined?

[mattulbrich]

1. I am not sure. In static Java contexts, one does not have type variables available. I'd say, no.
2. Yes, as usual earlier clauses can guard later clauses. That is for implicit invariants we should have the order:

   /*@ requires a != null; // implicitly
   @ requires \invariant_for(a); // implicitly
   @ requires \invariant_for(this); // implicitly
   @ requires manualspecification;
   @ ...
   @*/
   void m(Object a);

[leavens]

I think the opposite for question 1, as static contexts are the only ones in which type parameters are available. They are not present at runtime (sadly).

For the second question, thus far we have not defined an ordering between multiple supertypes (which can happen if types implement several interfaces). But this could be done if necessary. It might be needed for some invariants to protect others from being ill-defined (or having exceptions).

[mattulbrich]

Static is an overloaded notion here: I used static as in the static keyword in Java: The class invariant that deals with the static fields of the class is the static invariant, which can be used in static analysis (the 2nd notion of static) and dynamic analyses.

So: Yes type parameters can only be used in static analyses, but type parameters are not available for the static fields and methods of a class.

[mattulbrich]

For the second question, thus far we have not defined an ordering between multiple supertypes (which can happen if types implement several interfaces). But this could be done if necessary. It might be needed for some invariants to protect others from being ill-defined (or having exceptions).

That's interesting. I would say that guarding does not go beyond contract borders so that the order of contracts would not be important. ... But maybe there is some effect somewhere.

[leavens]

Static is an overloaded notion here: I used static as in the static keyword in Java: The class invariant that deals with the static fields of the class is the static invariant, which can be used in static analysis (the 2nd notion of static) and dynamic analyses.

Ah, sorry for my misunderstanding of what you were saying. Yes, in a static invariant the type parameters would not be available for static fields and static methods of a class.

However, David's original question was in the actual argument type passed to \static_invariant_for, should that argument type be fully parameterized? Mattias, are you saying that it doesn't matter, because the invariant can't use the type parameters? I think we could possibly need them to verify uses of \invariant_for, so for consistency I would advocate that they also be required on arguments to \static_invariant_for.

[leavens]

For the second question, thus far we have not defined an ordering between multiple supertypes (which can happen if types implement several interfaces). But this could be done if necessary. It might be needed for some invariants to protect others from being ill-defined (or having exceptions).

That's interesting. I would say that guarding does not go beyond contract borders so that the order of contracts would not be important. ... But maybe there is some effect somewhere.

I was thinking that if there are multiple supertypes of a type, then the ordering of those could be used to ensure that some conjuncts in a type's instance invariant of a type are well-defined. But it is reasonable to do as you say and not assume that one invariant can protect another, at the price of repeating some conjuncts in an invariant that are needed to protect various conjuncts.

[wadoon]

Parsing hint: \static_invariant_for(<type>) is a special case in the grammar.

Normally, a JML function call expr (or in Java terms a method call expr) has a name and arguments as expressions. But a type name is not an expression, the nearest Java expression would be the access of T.class field.

Therefore, \static_invariant_for(Type) requires a special treatment in the grammar. I am currently only aware of one similar case: \type(TYPE). Of course, we can avoid an additional special case by using \invariant_for(\type(T)) instead of \static_invariant_for(T).

[davidcok]

On the parsing issue: Yes - but no big problem. Java itself has situations in which only type-names are parsed, such as declarations and type parameters. And there are other similar anomalies in JML besides \type -- \old and \fresh with labels are another, as they take a label name, not an expression

[davidcok]

1) Upon remembering that, unfortunately, Java does not make type parameters available in static contexts, I'm going to advocated that the type name in \static_invariant_for may, but need not be an erased type name. That is one can write, equivalently, \static_invariant_for(List) or \static_invariant_for(List<integer>), but not \static_invariant_for(List<T>) (for a type variable T).

2) I advocate that within a class, invariants be conjoined in textual order (distinguishing static and non-static invariants). I think it natural and intuitive and I find it common to break up a long invariant of many conjunctions into separate ones for readability. It certainly saves repetition.

3) I also advocate that instance invariants may rely on static invariants being true. For example, one might have

static int MAX;
//@ static invariant 0 <= MAX <= 1000;

then non-static invariants may use MAX and use the fact of the static invariant without always having to write ``\static_invariant_for(X) ==> ...

4) For the same reasons, I think that the conjoining of instance invariants of a class may assume the instance invariants of its super types, in no defined order, recursively.

[leavens]

All that @davidcok says in the preceding item makes sense to me and I'm okay with it.

The ordering does matter, since we are using short-circuit evaluation for conjunction (&&), and JML's semantics for specification expressions allows for exceptions, so the author of a specification expression needs to be sure if the check for something (say a static field being null or 0) occurs before it is used (say in a dereference or division) that could cause an exception. We might suggest, in an example, that if one of the static invariants for some supertype includes such a conjunct, then it be mentioned explicitly in a static invariant of the subtype that occurs textually before the other (instance/dynamic) invariants for that subtype.

[wadoon]

Just to make this explicit.

With #3, we could add \invariant_for(obj, A) to retrieve a specific invariant with name A from obj. The consensus of #3 was not to use the names in JML (at least for the moment), so we would not add the this notion. Right?

[mattulbrich]

I like \invariant_for(obj, A) and since #18, there are names. But this should be a new issue, not static invariants.

[mattulbrich]

To David's comments:

Ad 1. The static invariant for List<String> is exactly the same as that for List. People might get a wrong impression if the former can be used despite not making a reference to Strings. A warning should be issued and then continued; like accessing a static variable via an object.

Ad 2. Textual order: of course.

Ad 3+4. So you would say there is an implicit clause //@ invariant \static_invariant_for(MyClass); ? and another implicit clause //@ static invariant \static_invariant_for(MySuperClass);? The constructor should then have an implicit precondition //@ requires \static_invariant_for(MyClass). I am reluctant since this would require a LOT of dragging static invariants around.

Who establishes these invariants anyway? And when? KeY has support for verifying static initialisers but that is extra overhead.