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/20 14:28] vkuncak |
sav07_lecture_3_skeleton [2007/03/20 14:32] vkuncak |
||
---|---|---|---|
Line 37: | Line 37: | ||
assert false = crash (stops with error) | assert false = crash (stops with error) | ||
+ | |||
assume true = skip (does nothing) | assume true = skip (does nothing) | ||
+ | |||
+ | ==== Composing formulas using relation composition ==== | ||
+ | |||
+ | This is perhaps the most direct way of transforming programs to formulas. | ||
+ | It creates formulas that are linear in the size of the program. | ||
+ | |||
+ | Non-deterministic choice is union of relations, that is, disjunction of formulas: | ||
+ | |||
+ | CR(c1; c2) = CR(c1) | CR(c2) | ||
==== Papers ==== | ==== Papers ==== |