Using KeY for Verification

As the Z3 provides a different approach on arrays than Java, we might better use KeY for the verification of the contracts by generating methods and classes out of the contracts and verify them. Therefore we could generate a new Visitor which parses our grammar.

For example the Z3 doesn't allow an array.length evaluation, or an array sum or the min and max value of an array.