team-worthwhile/worthwhile — Issue #72: Race condition when settings prover result markers in editor
Author: leonhandreke
Created: 2012-02-19 10:57:06+00:00
State: open
Labels: ui

Given the following code:

```
function Boolean is_prime(Integer a)
_requires a > 1
_ensures (∀ Integer q, (q < a) ∧ (q > 1): a % q ≠ 0) ⇒ (_return = true)
_ensures (∃ Integer l, (l < a) ∧ (l > 1): a % l = 0) ⇒ (_return = false)
{
Integer i := 2
while (i < a) {
if (a % i = 0) {
return false
}
i := i + 1
}
return true
}

Boolean res := is_prime(11)
_assert res = true
```

the UI sometimes marks the _ensures in green and at other times in red. This is because multiple proofs with the same related node (in this case, the precondition) yield different results. Somehow, a race condition occurs when coloring the code in the editor.

The UI should only apply the color signaling the "worst" outcome, i.e. red if at least one proof failed.