Missing explanations of statements and declarations#29
Conversation
…-declarations, more flexible declarations and assignments
| @@ -1 +1 @@ | |||
| # Top-level declarations | |||
There was a problem hiding this comment.
(Maybe we should add a comment at the beginning here to say that this is just a quick overview and that each subsection here just summarises a full section that appears later?)
There was a problem hiding this comment.
Yes, good point, will do.
|
|
||
| A `label` statement declares a program point with the given name. Labels serve two purposes: they can be the target of `goto` statements, and they can be referred to in [labelled old expressions](./expressions-multi.md) `old[l](e)`. A `goto` statement transfers control to the given label. Since Viper is primarily an intermediate language, gotos are mainly intended for encoding the unstructured control flow of front-end languages (for example, `break` and `continue` statements, or early returns); Viper programs must not use gotos to create *irreducible* control flow (e.g., jumps from outside a loop into the middle of the loop body). | ||
|
|
||
| A `goto` that jumps out of a `while` loop exits the loop *without* checking the loop invariant; permissions held before the loop that were not transferred into it via the invariant become available again after the jump. Loops can also be created by jumping *backwards* to a label. To support invariants for such loops, `label` declarations may be directly followed by `invariant` clauses; a label's stated invariant is used only if the label is in fact a loop head. Both features are illustrated in the following example: |
There was a problem hiding this comment.
Warn that using this feature carelessly might lead to unsoundness? (E.g., invariant on a label that is not actually a loop head, trying to place multiple invariants in the same CFG loop, ...)
There was a problem hiding this comment.
Might it? If you put an invariant on a label that's not a loop head it should simply be ignored. The text could make that clearer, but that should not make anything unsound. Nor should placing multiple invariants in the same loop afaik? If it does, that sounds like a problem we should fix yesterday.
There was a problem hiding this comment.
Didn't you talk with Jonáš about this recently? x) Even so, the silently ignoring part should be addressed and pointed out here as a (current) limitation. Maybe it's not strictly unsound but...?
method test() {
var x: Int := 0
label head
invariant 0 <= x <= 10
label body
invariant false // this is fine
if (x >= 10) {
goto end
}
x := x + 1
goto head
label end
assert x == 10
}
There was a problem hiding this comment.
Okay, yes, we should say it's silently ignored. And we could also just fix that and emit a warning when we see an invariant on a non-loop-head.
But it's an auxiliary proof annotation. No postcondition and no assert verifies that shouldn't verify, IMO there is absolutely nothing unsound going on here.
There was a problem hiding this comment.
There was a problem hiding this comment.
I guess we can adapt and merge this once we've discussed whether it should be a warning or an error.
2 participants
Missing information on top-level declarations like ADTs, abstract methods.
More flexible forms of variable declarations and assignment statements.
Labels and goto statements.