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.)

[leavens]

You are both right that we don't want pure to imply heap_free. I was confused, sorry.

I think we all agree that we want to avoid exceptional behavior when reasoning about (or executing in RAC) specification annotations. We could require that every pure method have at least one normal_behavior specification case and that a call in a specification annotation satisfies the precondition of at least one of these normal_behavior specification cases. This seems to be what Mattias is proposing. David seems to be proposing that the state at the call site imply that no exception can be thrown, based on the specification of the pure method being called. Is that right?

[mattulbrich]

No, I'd rather support the second statement: A well-defined specification should mention a method only with arguments such that one normal_behaviour specification case has a satisfied precondition. A pure method needs not have a specification case for all inputs, let alone a normal_behaviour case.

[davidcok]

Mattias - do you mean then that within a specification only normal_behavior spec cases are considered? Ignoring any behavior or "lightweight" cases? I can live with that -- and it is easy to give a warning during type-checking if there are no normal spec cases for a method with a pure modifier.

[mattulbrich]

On 31.03.22 00:32, David Cok wrote:

Mattias - do you mean then that within a specification only normal_behavior spec cases are considered? Ignoring any behavior or "lightweight" cases? I'd say that any lightweight/behaviour cases with signals false would be considered normal.

[davidcok]

OK. But you are saying that the signals false in the lightweight/behavior case must be explicitly written by the user; it is not implied by the pure modifier. Correct? Gary do you concur?

If so:

• pure does not imply specific exception clauses (though it does imply assignable \nothing and forbids any diverges clause other than diverges false (which is the default))
• but when used in a specification, only cases that are normal_behavior or have explicit signals false or signals_only \nothing are used to scribed the method's result

[mattulbrich]

Yes, I believe the default specification for signals is "true", and I do not think that the pure modifier should change the default value.

Moreover: I strongly believe that people should make clear if the contract they write is normal or exceptional (or mixed). It would be confusing if that depended on "pure".

pure is short for / implies writing "assignable \nothing" so that this is not a change of defaults, it is a concrete clause that is assumed. I think you cannot give another assignable clause on a pure method.

I have not thought about diverges yet, but that seems to be the same: pure adds an diverges clause and does not change the default.

but when used in a specification, only cases that are normal_behavior or have explicit signals false or signals_only \nothing are used to scribed the method's result

This sounds very reasonable.

[davidcok]

We left this issue with somewhat of a consensus: a specification case is ignored when a pure method is used in a specification unless it is 'effectively normal' --- that is, the case is a normal_behavior or has a signals_only \nothing clause or has a signals (Exception) false clause.

I worked on adjusting OpenJML to this rule and have the impression that it is confusing and has poor usability. Silently ignoring spec cases is a recipe for confusion. If a simple getter function is given a simple spec

//@ ensures \result == t;
//@ pure
public T getT() {
  return t;
}

the spec is ignored when the method is called in other specs. In addition, reasoning about a method call in Java code now is now different than reasoning about it in specs, even for non-exception-throwing behavior. I implemented a warning and now see that I have to fix a significant fraction of OpenJML's test cases. Essentially, every pure method needs a 'public normal_behavior' header. Also some reasonably pure library methods, like Collection.contains() permit their subclasses to throw exceptions at the subclass's discretion, making it impossible to give them a normal_behavior spec.

I think an easier semantics is this. When a pure method is called in a specification, it is assumed not to thrown an exception. This keeps the semantics between calls in specs and in code the same, except that exceptions might be thrown in code. A lot less confusion and easier usability in writing specs.

It is simpler than some alternatives that only go part way (which we discussed before), like -- normal_behavior is the default for lightweight specs cases of pure methods -- signals false and signals_only \nothing are the defaults for pure methods Going with what I proposed above, we would not need these either.

The only problem I can think of is that the assumption that a method does not throw an exception makes it infeasible. But that can happen anyway (even without the change I propose), with any spec that is equivalent to

public normal_behavior
  ensures false;
pure

[leavens]

Your point about simple specifications for getters is well taken. How is it that ESC assumes that a pure method called in a specification does not throw an exception; that is, what is the mechanism used? What happens in RAC?

Otherwise this proposal sounds good to me.

[mattulbrich]

David, why is a pure method so different from a non-pure method? We have to write normal_behaviour for a method contract that does not throw an exception. Why is that any different for pure methods?

I agree that it should be detected that a method is only called within a contract that allows application. The well-definedness check for a pure method call o.m() in a specification should thus be the disjunction of all contracts that are effectively normal. Thus, if one omits the normality, then a warning will be raised. This warning can naturally say something like "pure method call in specification outside the non-exceptional specification cases" or something like this.

I'd say that of course most pure methods need a normal_behavior specification case since they should not throw an exception.

I think I do not understand your proposal. Would that mean that we assume a postcondition for a method although it actually might throw an exception. Is the following then a correct program? If not, why not?

class X {
    //@ behaviour
    //@  ensures false;
    //@  assignable \nothing;
    int m() { throw new RuntimeException(); }

    //@ normal_behaviour
    //@  ensures m() == 42;
    //@  ensures m() != 42;
    void problem() {}
}