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

Local variables of the function should be visible in the postcondition #16

Closed jspam closed 12 years ago

jspam commented 12 years ago

Since the postcondition is actually just an _assert at the end of the function, variables declared in the function's main block should be visible there.

This affects scoping and the interpreter.

bafain commented 12 years ago

No, variables local to a function's body should not be visible in its annotations. In the scope of the function's postconditions only the function's parameters and the function's return value are visible. This is especially important when function calls are transformed during the calculation of some block's weakest precondition, because then both the pre- and postconditions are inserted instead of the function's body. Worthwhile decided to have a modularized look on functions and maybe it is intuitive that function implementations can change while their contract does not, assertions that refer to function local variables are only of interest when the function is validated and not a program calling that function.

jspam commented 12 years ago

Okay, though it will probably be difficult to prove BubbleSort then (see the example program in the wiki)