Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:proof_and_code_generation_in_lcf_systems [2009/03/05 13:45] vkuncak |
sav08:proof_and_code_generation_in_lcf_systems [2009/03/05 13:52] (current) vkuncak |
||
|---|---|---|---|
| Line 39: | Line 39: | ||
| then this shows that function deriveFact always produces a valid theorem. Whenever we use expression on LHS, we could hace used expression on RHS. While RHS constructs a theorem, the LHS directly computes it, without invoking primitive rules, so it can be much faster. It is the theorem prover in the usual sense. | then this shows that function deriveFact always produces a valid theorem. Whenever we use expression on LHS, we could hace used expression on RHS. While RHS constructs a theorem, the LHS directly computes it, without invoking primitive rules, so it can be much faster. It is the theorem prover in the usual sense. | ||
| + | |||
| ===== Proving Software ===== | ===== Proving Software ===== | ||
| Line 56: | Line 57: | ||
| - 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 | ||
| - no need to trust verification-condition generator | - no need to trust verification-condition generator | ||
| - | - limitations in terms of generated code | + | - limitations in terms of generated code, especially to generate imperative and concurrent code |
| - need to trust code generator | - need to trust code generator | ||