Simpler sort syntax

[mattulbrich]

Intended Change

This PR suggests changing the type parameter syntax from T<[X]> to T<X> for readability reasons.

(The original syntax was suggested to avoid parser problems wrt implicit identifiers like <init>.)

Plan

• Changed the lexer and parser
• Repaired >= and >>
• Adapting the toString methods
• Adapting many, many references in examples and test cases

Type of pull request

• Refactoring (behaviour should not change or only minimally change)

Ensuring quality

• yes: I made sure that introduced/changed code is well documented (javadoc and inline comments).
• n/a: I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• yes: I added new test case(s) for new functionality.
• no: I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[WolframPfeifer]

I really like this feature. However, we should consider the following (motivated by experience with VeriFast, compare also to verifast/verifast#271):

Assuming we want to lift this syntax into JML (for instance for ghost fields and model methods), it might be unexpected for the user that the List<T> in Java is quite different from \seq<S> in JML. The upper bound of T is Object, while the upper bound of S would be any.

A problematic example would be (not real JML for the sequence singleton, access and concat):

class List<T> {
  //@ ghost \seq<T> absVal;

  //@ ensures absVal == \old(absVal) ++ (t);  // <-- This is ok.
  void add(T t) {
   ..
  }

  //@ ensures \result == absVal[i];      // <-- Probably still ok here ...
  //@ assignable \nothing;
  T get(int i) {
   ..
  }
}

[WolframPfeifer]

Actually, in the example above it might not be a problem, because T in the ghost field is inside the scope of the class, so it is actually the same T here.

[Drodt]

The consensus is that this PR should be merged once ready.

[wadoon]

Wolfram's point was already discussed some time ago, where we discovered that the implicit upper bound between Java (java.lang.Object) and JML (in KeY any) is different.

Let us assume the following:

class Box<T extends ?>{ 
   //@ \dl_seq<T> s;

   //@ ...
   //@ <Q extends ?> model \dl_seq<T> t();
}

The following is valid T <: Object but not Q <: Object.

We discussed the introduction of additional type parameter parentheses. But maybe playing around with JML/Java syntax could avoid the confusion:

1. Java/JML Syntax: Box<T extends ?> is always Object-bound
2. A logical bound type must be stated explicitly: Box<T extends \dl_any> or also using the typeof operator: Box<T <: \dl_any>.

[mattulbrich]

Thanks Richard for repairing the term hash scheme such that all examples run through.

I have tried to adapt the proof, but the automation happens to do things in a slightly different order and then rewriting can no longer establish the needed statements. I can close the proof manually with a few rule applications that contradict the then natural order of the rules, but this is quite difficult to capture in a proof script or lemma.

This case shows that (as discussed only yesterday), our equality treatment is very brittle.

Thanks again, Richard!

The PR is ready now.