Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav07_lecture_3_skeleton [2007/03/21 10:53] vkuncak |
sav07_lecture_3_skeleton [2007/03/21 11:01] vkuncak |
||
---|---|---|---|
Line 2: | Line 2: | ||
===== Converting programs (with simple values) to formulas ===== | ===== Converting programs (with simple values) to formulas ===== | ||
+ | |||
Line 11: | Line 12: | ||
* we can represent relations using set comprehensions; if our program c has two state components, we can represent its meaning R( c ) as $\{((x_0,y_0),(x,y)) \mid F \}$, where F is some formula that has x,y,x_0,y_0 as free variables. | * we can represent relations using set comprehensions; if our program c has two state components, we can represent its meaning R( c ) as $\{((x_0,y_0),(x,y)) \mid F \}$, where F is some formula that has x,y,x_0,y_0 as free variables. | ||
- | * this is what I mean by ''simple values'': later we will talk about modeling pointers and arrays, but we will still use this as a starting point. | + | * simple values: variables are integers. Later we will talk about modeling pointers and arrays, but what we say now applies |
Our goal is to find rules for computing R( c ) that are | Our goal is to find rules for computing R( c ) that are | ||
Line 102: | Line 103: | ||
This idea is important in static analysis. | This idea is important in static analysis. | ||
+ | |||
+ | |||
Line 112: | Line 115: | ||
Symbolic execution converts programs into formulas by going forward. It is therefore somewhat analogous to the way an [[interpreter]] for the language would work. | Symbolic execution converts programs into formulas by going forward. It is therefore somewhat analogous to the way an [[interpreter]] for the language would work. | ||
+ | Avoid renaming all the time. | ||
+ | |||
+ | SE(F,k, c1; c2) = SE(F & R(c1), k+1, c2) (update formula) | ||
+ | |||
+ | SE(F,k,(c1 [] c2); c2) = SE(F, k, c1) | SE(F,k,c2) (explore both branches) | ||
+ | |||
+ | Note: how many branches do we get? | ||
Strongest postcondition: | Strongest postcondition: | ||
Line 119: | Line 129: | ||
Like composition of a set with a relation. It's called ''relational image'' of set $P$ under relation $r$. | Like composition of a set with a relation. It's called ''relational image'' of set $P$ under relation $r$. | ||
- | Note: when proving our verification condition, instead of proving that semantics of relation implies error=false, it's same as proving that the formula for set sp(U,r) implies error=false, where U is the universal relation. | + | Note: when proving our verification condition, instead of proving that semantics of relation implies error=false, it's same as proving that the formula for set sp(U,r) implies error=false, where U is the universal relation, or, in terms of formulas, computing the strongest postcondition of formula 'true'. |
==== Weakest preconditions ==== | ==== Weakest preconditions ==== | ||
While symbolic execution computes formula by going forward along the program syntax tree, weakest precondition computes formula by going backward. | While symbolic execution computes formula by going forward along the program syntax tree, weakest precondition computes formula by going backward. | ||
+ | |||
+ | wp(Q, x=t) = | ||
+ | wp(Q, assume F) = | ||
+ | wp(Q, assert F) = | ||
+ | wp(Q, c1 [] c2) = | ||
+ | wp(Q, c1 ; c2) = | ||
==== Inferring Loop Invariants ==== | ==== Inferring Loop Invariants ==== |