*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Some Remarks to Code Generation*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Wed, 01 Aug 2012 11:12:25 +0900*In-reply-to*: <op.wibki8x0ule2fv@douda-yannick>*References*: <234E321B-095C-4FBC-9DBC-CD3E5693D8D6@pbmichel.de> <op.wibki8x0ule2fv@douda-yannick>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:14.0) Gecko/20120717 Thunderbird/14.0

On 08/01/2012 01:38 AM, Yannick Duchêne (Hibou57) wrote:

Le Tue, 31 Jul 2012 18:13:12 +0200, Patrick Michel <uni at pbmichel.de> 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?

definition ite where "ite b x y == if b then x else y" lemmas ite_cong [fundef_cong] = if_cong [folded ite_def] fun f :: "nat => nat" where "f x = ite (x = 0) 1 (f (x - 1) * x)"

[...] partial correctness of the generated programs w.r.t. the original equational theorems is guaranteed. No claims are stated for aspects which have no explicit representation in the logic, in particular termination or runtime complexity. cheers chris

**Follow-Ups**:**Re: [isabelle] Some Remarks to Code Generation***From:*Magnus Myreen

- Previous by Date: Re: [isabelle] Isabelle's jEdit plugin: some known help documents?
- Next by Date: Re: [isabelle] Isabelle's jEdit plugin: some known help documents?
- Previous by Thread: Re: [isabelle] Isabelle's jEdit plugin: some known help documents?
- Next by Thread: Re: [isabelle] Some Remarks to Code Generation
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list