Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Last revision Both sides next revision | ||
sav08:proof_and_code_generation_in_lcf_systems [2008/05/28 11:09] vkuncak |
sav08:proof_and_code_generation_in_lcf_systems [2009/03/05 13:45] vkuncak |
||
---|---|---|---|
Line 52: | Line 52: | ||
- use interactive proof to prove these verification conditions | - use interactive proof to prove these verification conditions | ||
- | Aprooach 1 is | + | Characteristic of Aprooach 1: |
- more flexible: we choose how to organize the proof, need not use particular VCGen strategy | - more flexible: we choose how to organize the proof, need not use particular VCGen strategy | ||
- can be more difficult to combine with program analyses: program analysis may need to be programmed as a tactic in the interactive prover | - can be more difficult to combine with program analyses: program analysis may need to be programmed as a tactic in the interactive prover |