function / no_state / reads \nothing

[davidcok]

We need a method modifier that denotes methods that do not reference the heap. This is an element of specification in that it lies at the interface of the method -- and can be used by clients and verified against the implementation.

A method marked this way is known to be independent of the heap -- so its value (for the same arguments) does not change when the heap changes. This means also that it does not depend on fields of any reference-type arguments.

All operations on builtin mathematical types are in this category.

Also, operations on 'immutable' types such as String and integer, whose heap state, if any, is unobservable by anything else.

The question is: how should this be specified in JML.

1) OpenJML is using function 2) I think KeY is using no_state 3) And does reads \nothing (that is accessible \nothing;) accomplish the same goal, if more obscurely?

[wadoon]

I find the heapless modifier as a more direct description.

ad (2). To understand KeY's choice, you should now that there is a also two_state modifier.

ad (3). Depends on the semantics of reads \nothing and accessible \nothing. Does accessible is always a super set of assignable? Does accessible only refers to existing objects? (Note, KeY's difference on assignable \nothing to assignable \strictly_nothing)

[leavens]

I agree that heapless would be a good modifier for this, or perhaps heap_free. Either function or no_state is fine also.

[mattulbrich]

I agree that heapless is a good modifier and sounds self-explaining.

(or heap_free or no_heap). Alexander is right about two_state, but that does not really require no_state as a counterpart. I do not really like function as a modifier for such methods, because that is (in Dafny, Pascal-ish languages, ...) usually used for a pure method which may observe but not modify the state (including the heap).

It does (imo) not make sense to include not-yet instantiated objects into read/accessible clauses since any newly created value would have to be written before being read; so no dependency even possible. A method can have totally independent accessible and assignable sets (in KeY), if that makes sense is another matter.

@davidcok How do you feel about heapless?

[davidcok]

Of the choices heap_free, no_heap, heapless, no_state, function I'll pick heap_free as having the best connotation.

My understanding of this modifier is that the result of a method so modified does not depend on any mutable part of the the heap (or change the heap, including adding visible new allocations).

So, for a reference types

class T {
   int t;
   final int f;
}

boolean m(T a, T b) { return a == b; } is heap_free

boolean m(T a, T b) { return a.f == b.f; } is heap_free

boolean m(T a, T b) { return a.t == b.t; } is not

void m(T a, T b) { a.t = b.t; } is not

int m(T a) { return a.f; } is heap_free

int m(T a) { return a.t; } is not

T(int x} { t = x; f = x; } is not

also any methods on an immutable reference type, such as String and Integer are heap_free, as are any methods/operations on Java primitive types and JML built-in value types (e.g. \seq)

[mattulbrich]

I agree that boolean m(T a, T b) { return a.f == b.f; } should be heap free. In current KeY, it isn't since final fields are fields after all. That may change in future.

Does it make sense to annotate non-pure functions with this modifier at all? If so, then I'd say that { this.x = 42; } is heap_free since it does not read anything from the heap, and its effect does not depend on it.

Another question is if { return this.x == this.x; } is heap_free. KeY says yes (since the result does not depend on the heap. An explicit access check may yield no. This is a pathological corner case which would endanger soundness but changes the set of accepted methods slightly.

[mattulbrich]

Semantically, I think it is clear that heap_free would be desugared to accessible \nothing; (or reads if we change the keyword). Right?

[leavens]

The syntax heap_free seems to be somewhat of a consensus and sounds good to me. However, allowing dependencies on immutable fields in the heap seems to make this complex and perhaps harder to remember. The KeY semantics of disallowing all dependencies on fields seems simpler.

I would think that heap_free should only be allowed on pure functions, for simplicity, and to allow the desugaring that Mattias discusses (to accessible \nothing).

[davidcok]

The rationale for permitting access to immutable/final fields in heap_free is that final fields are frequently used as symbolic constants -- it seems a bad design if the whole specification needs to change because an explicit constant is changed to a symbolic constant.

The practical purpose behind having heap_free is whether a logical representation of a method (as a logical function) needs to have a representation of the heap as an explicit or implicit argument -- for which purpose perhaps the key criterion is whether there are any '.' or array dereferences at all, final or otherwise.

Which leaves me a bit undecided.

[davidcok]

On heap_free vs accessible \nothing.

I would think that boolean m(T a, T b) { return a == b;} is heap_free but is accessible a, b; so those would not be equivalent? Or does KeY allow omitting from a reads clause local variables and formal parameters (including this)?

[mattulbrich]

On 23.02.22 15:53, David Cok wrote:

The rationale for permitting access to immutable/final fields in heap_free is that final fields are frequently used as symbolic constants -- it seems a bad design if the whole specification needs to change because an explicit constant is changed to a symbolic constant.

I think we should differentiate between static fields and compile-time constants. The latter are really only abbreviations for the value they abstract from. These are themselves heap-independent. We have a rule replacing Classname.CONST by the defined value.

(Disclaimer: I have no idea how this works for String constants which are special thanks to that string pool thing in Java.)

Which leaves me a bit undecided.

I can understand this. But compile-time constants may be the trick to resolve it?

[mattulbrich]

In KeY, location sets only contain locations on the heap. Stack location need not be mentioned. (We do an obvious inference there.) Of course, if a.x was mentioned in the code then that would have to be covered by the clause, but comparing the values (i.e. the addresses or object identities) is heap-independent.

[davidcok]

Compile-time constants are perhaps a place to start. A bit of experience is needed her, at least on my part.

If heap_free does not allow a dereference of a final field, then at least I want to argue that final fields are not part of assignable \everything

[mattulbrich]

Well. assignable \everything means you are allowed to changed in a program any heap location that you can modify. Since the value of a final field cannot be modified, one can safely assume that the value of a final field is the same after a method call by the semantics of Java.

(That is: If we disregard reflection, which we definitely should do ...)

[leavens]

Mattias's comments seem sensible to me.