LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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