Re: [isabelle] Some Remarks to Code Generation


Here is a small example:

theory Scratch imports Main

fun fib :: "nat \<Rightarrow> nat" where
 "fib 0 = 0"
| "fib (Suc 0) = Suc 0"
| "fib (Suc (Suc n)) = fib (Suc n) + fib n"

value "map (fib o nat) [0..10]"

theorem fib_loop [code]:
 "fib n = fib n"
 by simp

export_code fib in Scala file "Fib.scala"


Patrick Michel

On 31.07.2012, at 18:38, Yannick Duchêne (Hibou57) wrote:

> Le Tue, 31 Jul 2012 18:13:12 +0200, Patrick Michel <uni at> a écrit:
>> As it turns out it is quite easy to prove a code equation that obviously leads to non-terminating execution.
> I've not reached that point (still learning Isabelle and HOL), but I'm already interested in this, as I will generate SML programs from proofs. Can you please, provide a concrete example of an erroneous proof of a non‑terminating function?
> -- 
> “Syntactic sugar causes cancer of the semi-colons.” [1]
> “Structured Programming supports the law of the excluded muddle.” [1]
> [1]: Epigrams on Programming — Alan J. — P. Yale University

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.