search

team-worthwhile / worthwhile

PSE am KIT 2011/12: Programmverifikation (Team 2)
BSD 3-Clause "New" or "Revised" License
5 stars 3 forks source link

WPStrategy::visit(Loop) reuses AssignedVariables with their initial value set #101

Closed bafain closed 12 years ago

bafain commented 12 years ago

"Prove it!" the following Worthwhile specification and inspect the partial prove result for the loop.

Integer a := 0
while (false) {
    a := 1
}

The displayed string result includes the variable a's initial value.

Verifying that invariant and loop condition imply the loop body’s postcondition:

∀ Integer a := 0 : false ∧ true ⇒ true

Proof attempt for the calculated formula resulted in Validity VALID

Prover output was:
unsat
(error "line 3 column 10: model is not available")

Because we do not distinguish between variable and variable declaration in the model we do not in AstNodeToStringHelper either, which is used here for rendering.

leonhandreke commented 12 years ago

Where exactly is the problem with that? As long as I bind it with a forall quantifier, this shouldn't be a problem, should it?

bafain commented 12 years ago

This is right, there is no problem with that in the program transformation or formula compilation since the prover ignores initial values set for quantifier parameters (the ambiguity of VariableDeclarations mentioned above that is).