Differences
This shows you the differences between two versions of the page.
Next revision Both sides next revision | |||
sav08:proof_and_code_generation_in_lcf_systems [2008/05/28 05:39] vkuncak created |
sav08:proof_and_code_generation_in_lcf_systems [2008/05/28 11:09] vkuncak |
||
---|---|---|---|
Line 14: | Line 14: | ||
Modern LCF-based provers such as Isabelle contain 'reflection' capabilities as an additional feature. | Modern LCF-based provers such as Isabelle contain 'reflection' capabilities as an additional feature. | ||
+ | |||
+ | ===== Proving Provers ===== | ||
If we prove, within the system, that certain executable function preserves the truth value of a formula, we can | If we prove, within the system, that certain executable function preserves the truth value of a formula, we can | ||
Line 19: | Line 21: | ||
* use the generated code as a built-in formula transformation | * use the generated code as a built-in formula transformation | ||
- | This was used within Isabelle in recent work "Linear quantifier elimination". | + | Such approaches were used within Isabelle in recent work on "Linear quantifier elimination". |
+ | |||
+ | More generally, suppose we have two functions | ||
+ | |||
+ | deriveFact : a -> theorem | ||
+ | computeFact : a -> formula | ||
+ | |||
+ | Suppose we have a an unsafe function | ||
+ | |||
+ | mkTheorem : formula -> theorem | ||
+ | |||
+ | that just postulates formula as a theorem. | ||
+ | |||
+ | If we prove that, for all a, | ||
+ | |||
+ | mkTheorem (computeFact a) = deriveFact a | ||
+ | |||
+ | 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 ===== | ||
+ | |||
+ | Approach 1: | ||
+ | - define executable functions (typically as pure, terminating, recursive functions) within HOL prover | ||
+ | - use interactive prove to show that functions satisfy desired properties | ||
+ | - automatically generate code for these functions | ||
+ | |||
+ | Approach 2: | ||
+ | - start with code in some programming language | ||
+ | - generate verification conditions in HOL | ||
+ | - use interactive proof to prove these verification conditions | ||
+ | |||
+ | Aprooach 1 is | ||
+ | - 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 | ||
+ | - no need to trust verification-condition generator | ||
+ | - limitations in terms of generated code | ||
+ | - need to trust code generator | ||