Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision Last 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 [2009/03/05 13:45] 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 | ||
| + | |||
| + | Characteristic of Aprooach 1: | ||
| + | - 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 | ||