captures and \only_captured

[davidcok]

The captures clause and \only_captured expression take store-ref-expressions as arguments. This seems wrong. It is object references that are captured (and aliased) not memory locations. Memory locations referring to primitive types are never 'captured' because the values are always copied.

[mattulbrich]

I must admit that I have not really known about these constructs yet.

The manual says: The captures clause says that references to the store-refs listed can be retained after the method returns, for example in a field of the receiver object or in a static field. Therefore, the captures clause specifies when an object, passed as an actual parameter in a method call, may be captured during the call.

I do not fully understand this semantics. What does captures o mean? I read this that no heap location may point to any other object, but to o? That seems very restrictive.

But regarding the required syntactical category, I think that David is right.

[mattulbrich]

Thought about it some more: Would captures o, p; perhaps be equivalent to a postcondition like (in pseudo-JML)

 (\forall Location l; l has existed in pre-state; valueOf(l) == \old(valueOf(l)) || valueOf(l) == o || valueOf(l) == p)

meaning that every modified reftype location either has not changed its value or points to a capture-allowed object.

Does that fit the bill?

[leavens]

The captures clause was intended to be used for alias control. @davidcok has the right idea: the intended meaning of captures o; was that the object to which o refers (which should be of a reference type) could be accessible to the this object after the method returns (in a field that might be static). I don't know how to explain that in general terms by referring to other concepts in JML.

Following the general JML design, this keyword should have been capturable (which is, according to dictionary.com a word!).

This clause is probably most useful when one writes: captures \nothing; I believe that is why the syntax used store-ref for what follows the keyword, but I agree that it should be the object that the store-ref refers to, not a field or location itself, that is capturable.

However, the captures clause is a very limited solution to the problem of alias control. Perhaps we should look for some better solution?

@mattulbrich captures doesn't have anything to do with modification, it has to do with aliasing. A method might capture an object reference and then (some other method that now has access to that object) modify it later, however.

[davidcok]

Good. For now (until we have a solid basis for a better solution for alias control), we'll say that the grammar is

captures [ \nothing | <expression> ... ] ;

where (type condition) each <expression> must have reference type. \nothing is just a clearer way of stating an empty list (captures ;)

When we have sets of objects defined for JML, we might allow an expression typed as \set<Object> in the list to mean all the elements of the given set are capturable (as is the case for \locsets in assignable clauses)

I have not yet investigated what checks are implied by this clause (other than the captures list for callees must be a subset of the list for callers, minding preconditions) or how it might simplify further verification.

@mattulbrich, if you are good with this, we can close this (and I'll adjust the RMv2 appropriately)

[mattulbrich]

Syntax-wise: I am happy.

Semantics-wise: What is the proof obligation for this clause? I can interpret Gary's answer (which gives some intuition), but I wonder how to deal with that in tools. What does accessible mean? (cf. \reach?)

[davidcok]

accessible is a framing condition that states what locations are read. Note that in Dafny, some constructs have 'reads' clauses that serve a similar purpose. A reads clause (for a heap-dependent function, for example) tells you whether the value of the function might have changed given some assignable frame. Dafny apparently uses this information as part of its reasoning, but I have never looked at the translation to understand why it is useful and important. OpenJML currently checks accessible clauses but does not make use of the information to help other proof obligations.

[mattulbrich]

I am sorry, I wanted to ask about captures and Gary's sentence

The captures clause was intended to be used for alias control. @davidcok has the right idea: the intended meaning of captures o; was that the object to which o refers (which should be of a reference type) could be accessible to the this object after the method returns (in a field that might be static). I don't know how to explain that in general terms by referring to other concepts in JML.

which uses the word accessible. Accidently, we have thus found and example for the point that typesetting keywords has its advantages since accessible and accessible are not the same. :grin:

We have accessible in KeY as well in the same fashion that Dafny uses them. It is mainly helpful to know that a function (or model field or invariant) has not changed its value although the heap has changed.

[leavens]

@mattulbrich i was using “accessible” in a general, semantic sense in what you quoted. I meant that an object o could potentially access another object p if there is some method that could be written in o’s class that could return p. This doesn’t correspond exactly to JML’s accessible clause, as that is more about permitting reads from a store-ref.

I would say that o captures p in o’s method m if in m’s pre-state p is not accessible in this (general) sense, but p is accessible in m’s post-state, I’m that same sense.

I agree with you about how JML’s accessible clause is used in reasoning. It’s mostly useful for understanding dependencies of abstractions, such as model fields and model methods.