`signals`-clause

[wadoon]

In the current state, JML ref manual states for the signals clause:

//@ signals (RuntimeException e) ... e ... ;
//@ signals (RuntimeException) ... \exception ... ;

---

1. I would like to re-align this to the catch-clauses. In particular, I want to allow multiple exceptions like in try { ... } catch(E1 | E2 e) { }.

   Therefore, I suggest:

   //@ signals (E1 | ... | En  e) <expr>;
   

   The type of e is the union of each type E1 to En as defined by JLS. Also note, that E1 to En have to be disjoint in catch-clauses.

   Concrete example:

   //@ signals (IllegalAccessException | IllegalStateException  e) !e.getMessage().isBlank() ;
   

2. I propose to make the exception variable mandatory, thus do drop the second line in the current description of the ref manual.

   For me, it seems to be a complicated special case. If anyone does not want to assign a name, they can use _ as an identifier to signal this circumstance.

   This change would not affect \exception.

3. I have a question:

   Assuming multiple signals clauses, do their exception type need to be disjoint?

   Example:

   //@ signals (IllegalStateException e) f1(e);
   //@ signals (RuntimeException e) f1(e);
   //@ signals (Exception e) f1(e);
   

   Note, that IllegalStateException <: RuntimeException <: Exception <: Throwable.

   This is legal for catch clauses. Java's semantics define that the first catch matching catch-block is executed.

   If we allow this for JML contracts, what are the semantics?

   • First/Java semantics: Only the first signals clause needs to be adhered to in the exceptional case.

     This makes the order of clauses important; I think that is currently not the case.

   • All semantics: Every matching signals-clause must adhere in exceptional cases.

     Under these semantics, we can normalize a given set of signals-clauses to one clause. The given example would become:

     //@ signals (Throwable t) 
            (t instanceof IllegalStateException t1 ==> f1(t1)) &&
            (t instanceof RuntimeException t2 ==> f2(t2)) &&
            (t instanceof RuntimeException t3 ==> f3(t3));
     

---

Side note: The pattern expression in Java makes the following expression well-typed:

x instanceof String s && s.isBlank()

Do we have defined that this is also well-typed for some JML-operators (in particular, the implication?):

x instanceof String s ==> s.isBlank()

This is not so obvious in the normal form: !(x instanceof String s) || s.isBlank().

[mattulbrich]

Discussion in Darmstadt: We can make the T ex in signals (T ex) phi optional. OpenJML has it optional already.

[davidcok]

Further information per a question from MU:

Exceptions are classes and not interfaces, thus there is always a "least common parent" for the list of possible exception types, which would be the type of the declared variable in the signals clause.

1 & 3) We proposed that the same rules be followed as in Java -- the exception types listed must be disjoint, that is no one of them is inherited from another.

2. I propose that signals clauses remain unordered, as now.

3. It is intended that the pattern matching work in JML as well, though I don't believe ==> does so as yet. || and && within a JML expression do work