Open mario-bucev opened 9 months ago
This does not seem like a huge problem to me. In the end, the user may want to see the verification condition. But I was not aware that we write "INVALID" only on the error position line. This may be making the issue more sensitive. In reality, the definitions and paths also affect the validity. I get, for example the report (with --no-colors, but the issue is same anyway):
warning: val y: BigInt = x + x
y + y >= BigInt("0")
Test.scala:8:13: warning: => INVALID
}.ensuring((y, z) => z >= 0)
Should this not be printed as:
warning:
Test.scala:8:13: warning: => INVALID
val y: BigInt = x + x
y + y >= BigInt("0")
}.ensuring((y, z) => z >= 0)
^
Namely, only the ^
sign affected by the position, not the "warning INVALID"?
The following snippet:
gives the following position for the VC:
which seems to say that
y
is responsible for the invalidity but is just an artifact of the postcondition position. If however we useval
s, we have:which is meaningful. On the other hand, we do not use
StaticChecks.ensuring
(whether we usevar
orval
), we get:so we get 3 different positions for small tweaks. If we can at least rule out 1, that would be great. If we can make it consistent, that would be even better (we should however choose between option 2 and 3, I'd say 2 is more consistent because this is the positions we get in presence of branches).