Skip to content

Invariants and old() #344

Closed Answered by bkragl
ghost asked this question in Q&A
Feb 16, 2021 · 1 comments · 5 replies
Discussion options

You must be logged in to vote

old(v) refers to the value of v at the beginning of the procedure (even before v := 0;). In your example this can be anything, because you do not have a precondition that talks about v. When Boogie checks the maintenance of the loop invariant, it could be that old(v) == 42 and v == 0 so the invariant holds, but after the loop body executes we have old(v) == 42 && v == 1 and the invariant does not hold anymore.

These are fundamental concepts, so you will find all the explanation you need in "This is Boogie 2".

Replies: 1 comment 5 replies

Comment options

You must be logged in to vote
5 replies
@ghost
Comment options

@bkragl
Comment options

@ghost
Comment options

@bkragl
Comment options

@RustanLeino
Comment options

Answer selected by bkragl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Category
Q&A
Labels
None yet
2 participants