exceptions in methods in specifications

[davidcok]

Methods called in specifications must (a) have no side effects and (b) be called in a well-defined manner.

The second point means that the calcite should fulfill the method's preconditions.

But also the method should not throw any exceptions.

So I propose
(a) when a method is called in a specification any exceptional_behavior spec cases are ignored
(b) a method declared pure has as default signals false and signals_only \nothing
(c) any behavior spec case of a pure method may not have any signals or signals_only clauses other than the defaults
(the method could still have exceptional_behavior cases for use outside of specifications)

[leavens]

I agree it would not make sense to have a method be called in a specification in order to generate an exception. The defaults mentioned in (b) make sense for that reason.

However, I think that (a) and (c) lose some of the algebraic properties of JML's design, I would prefer that (a) be rephrased to say that any spec cases in which the method may throw an exception (i.e., where signals is not provably false) be ignored and that (c) be rephrased to say that a behavior spec case has signals false and signals_only \nothing as the defaults.

[mattulbrich]

I seem to remember that at one point "pure" implied something like (b). But I think this confuses users and I do not think that we should change defaults.

If you have a pure method, just define its relevant contract "normal" and you are fine. If one chooses to leave out "normal"/"exceptional" etc. I do not think that it is a good idea to different meaning for specifications whether pure or not pure.

In KeY you can actually also use exceptional contracts, but that is perhaps a special element in KeY. ...

[leavens]

I agree that it complicates the language design to have different meanings for specifications for pure and not pure methods, so I agree that not having that complication would be a good thing. We could certainly encourage people to only specify pure methods using normal_behavior specification cases, but the language semantics needs to have a meaning for when that recommendation is not followed.

I don't recall that pure implied (b) prevoiusly, but I do remember that pure methods were supposed to be functional (deterministic) at some point in the past.

[mattulbrich]

Like David I think that pure methods may also have exceptional cases for when they are called from code, not specification. When used in specification only the normal specifications should be used. When used outside the precondition, this may either result in a welldefinedness warning or may produce an underspecified value.

[leavens]

I agree that if pure methods are intended to be used in code (esp. by untrusted clients) than having exceptional behavior specification cases makes sense for them. And I agree that it only makes sense to use the normal behavior specification cases when pure methods are called in specifications. If such a pure method would throw an exception during verification, we have a semantics for that.

[davidcok]

So pure methods
a) can have an exceptional_behavior case
b) such a case is not used in if the pure method is called in a specification.

What about simple 'behavior' cases?

• allowed to be used if the signals clause is false (or the signals_only is \nothing)?

-and the default is.... -- signals false for 'behavior' is pure methods. After all the assignable clause changes its default for pure methods.

[mattulbrich]

-and the default is.... -- signals false for 'behavior' is pure methods. After all the assignable clause changes its default for pure methods.

I think I do not understand that sentence.

I currently think that "pure" does not change the default, but is as good as specifying assignable \nothing.

[davidcok]

I was just wanting to raise the question of what the default should be.
But to use your wording, we can say that pure is as good as specifying signals false (except in an exceptional_specification case)

[mattulbrich]

To me this sounds like a rather complicated desugaring rule. "X is replaced by Y,Z unless A where it is only Y". mmmh.

I did recall wrong. The old manual required that a pure method always terminates. Dont know if that is really required for soundness reasons.

https://www.cs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_7.html#SEC60

[davidcok]

I think it is required for soundness (or at least helps the argument) -- making sure that all method calls in specs terminate.

[mattulbrich]

I think it is required for soundness (or at least helps the argument) -- making sure that all method calls in specs terminate.

I have been thinking about this quite a bit recently. A model method like

model int f() { return f() + 1; }

yields a definition axiom ∀ heap, o. o.f()@heap = o.f()@heap + 1 which is equivalent to false. Same is true for the model field

model int f;
represents f = f + 1;

This means that me making axioms out of their definitions, requires implementations of model fields and methods to be terminating (or rather wellfounded since they are not actually executed). And it is a soundness issue if that proof is not done.

Now, as for "normal" methods for which such a defining axiom does not exist: I believe they could get away w/o termination leaving non terminating cases under specified. Depending on the methodology one uses, termination is not soundness critical then.

Conceptually, I think it is a sensible restriction to require termination for everything in specifications (also for RAC).

That would additionally mean that one can only ever refer to pure methods from specs. assignable nothing would not be enough anymore since it is not a synonym anymore. ...

[leavens]

Yes, as Mattias's examples make clear, we need well-founded definitions of pure methods and represents clauses for soundness. In runtime assertion checking such definitions would ensure termination, which would also be very helpful for RAC.

I would say that sensible defaults for pure methods are to:
(i) make them assignable \nothing;,
(ii) make them heap_free, and
(iii) to warn about any calls to them in annotations (i.e., from specifications or assertions) that make a precondition of their specification case that allows an exception to be thrown true.
With (iii) we don't need to change the semantics of specifications for pure methods, but can give warnings about possibly suspect calls.

[davidcok]

I don't think you want (ii). Then, for example, any simple getter function would not be able to be pure.
Whereas, heap_free implying pure is what I proposed before, but Mattias demurred.

With (iii),

//@ ensures \result == x;
//@ pure
int x() { return x; }

is pure, but not allowed to be used in a specification because the (true) precondition allows an exception to be thrown.
That deviates from the previous implicit definition that methods marked pure could be used in specs.

Either
a) the user has to use normal_behavior
b) the user has to use signals false or signals_only \nothing
c) we make pure imply (b) -- which was my previous proposal

[mattulbrich]

Gary, I think there are very reasonable pure methods that have to access the heap. Like for an ArrayList

//@ pure
Object get(int index) { return content[index]; }

//@ ensures get(0) == x;
Object addFirst(Object x) { ... }

get is a pure method but needs the heap. Even pure model methods may require the heap.

Ad (i). I think this is the essence of pure methods.

Ad (iii). Let me reformulate it: "to warn about any calls to them in annotations (i.e., from specifications or assertions) that do not make a precondition of their specification case that disallows an exception to be thrown true." I.e. it suffices to have one case that disallows exceptions, not all of them.

In general, I wonder what this means in the face of many specification cases?

I'd say (i) applies to every specification case of the method, (iii) is a property of all callsites.

[mattulbrich]

In response to David (whose response came 20 seconds before mine ;) ):

I think that the user must use normal_behaviour (or other means) if they want to express that their method does not raise an exception. That is why we introduced that keyword. Pure or not pure.

(In KeY, you are allowed to refer to x() still. We are rather relaxed. However, you cannot count on the result being x because there might also have been an exception.)