In the annotationFailed and annotationSucceeded methods of the ExecutionEventListener, the prover output (which the interpreter gets from the SpecificationChecker) should also be passed in order to be shown in the GUI.
We would not need a special annotationFailed method then, but a method with a similar signature to this:
void assertionVerified(final Assertion assertion, final Validity validity, final ProverResult proverResult);
which the GUI could then handle in any way it wanted.
In the
annotationFailedandannotationSucceededmethods of theExecutionEventListener, the prover output (which the interpreter gets from the SpecificationChecker) should also be passed in order to be shown in the GUI.We would not need a special
annotationFailedmethod then, but a method with a similar signature to this:which the GUI could then handle in any way it wanted.