When loop condition + invariant is verified, the whole loop is marked in the UI

[jspam]

The prover reports its verification result of "loop condition and invariant imply block postcondition" with the statement parameter set to the loop. Thus, in the UI, the whole loop is marked, which a) does not look pretty and b) covers other markers in the loop, e.g. invariant markers.

[leonhandreke]

What should it cover? Would only the condition and the invariant be OK? (Yay, passing lists of related nodes requires yet another API change! Nothing to difficult though.)

[leonhandreke]

I think 37c687b is the wrong way to go about this. Internally, the prover already supports passing multiple related nodes. The UI shouldn't really know anything about what the specific proof means to the user, it should be stupid and just display whatever the proof generation strategy thinks is important for this specific proof.

Also, instanceof. Argh!

[jspam]

I think it’s okay that the prover passes the whole loop, the UI can figure out what to do with it by itself. The invariants shouldn’t be marked anyways, because they are already marked when invariantValidAtEntryVerified is fired.

[leonhandreke]

First of all, I think the invariants should also be marked. They, together with the invariants, have to imply the block postcondition.

The question is: Why should the UI even be able to figure it out? For all that it knows, the proof could have been conjured from thin air by a monkey with a typewriter. Maybe this monkey also wants to pass an invariant because he immediately sees that the invariant is too weak.

I think that simply passing a list of ASTNodes is the right way to go about this.

[jspam]

Well, don’t worry about instanceof; if that’s what bothers you, I’ll write a visitor which is only slightly more code …

But if you write

The UI shouldn't really know anything about what the specific proof means to the user, it should be stupid and just display whatever the proof generation strategy thinks is important for this specific proof.

, then we should do it the following way: IProverEventListener contains only one method, stuffVerified, with a list of nodes that it deems important for the current part of the proof. You will also have to supply the messages like "Verifying that loop condition and invariants imply the loop body’s postcondition" in the ProverResult.

[jspam]

On second thought, I’d rather name the method monkeyWithTypewriterVerifiedStuff in accordance with your previous example ;-)

[leonhandreke]

Yes, you are right. That would probably be the cleanest approach. However, that would put natural language into the prover implementation. The compromise I chose was to let the UI know what was proven (e.g. that the conditional and the invariants imply the block precondition) but not how (e.g. the monkey might give you only an invariant because it immediately saw that something was foul about it or even give you the assertion where the whole thing breaks down).

By deciding to only color the condition, the UI already makes a statement about the "how": It tells you that the condition was analyzed to be "incorrect" whatever that means. In reality though, the problem may lie somewhere totally different and the prover may not even have looked at the condition while creating the proof.

[jspam]

Okay, that sounds reasonable, could you make the necessary changes to IProverEventListener in a new branch? I can then fix WorthwhileProveJob accordingly.