*To*: "Jasmin Blanchette" <jasmin.blanchette at gmail.com>, "li yongjian" <lyj238 at gmail.com>*Subject*: Re: [isabelle] Formally proving the Boyer text matching algorithm*From*: "lyj238" <lyj238 at ios.ac.cn>*Date*: Wed, 28 Aug 2013 07:36:53 +0800*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*References*: <CABCjkDpsgdwyWu6vbCc4dKPuepxCA1+6psjOOW4J38zO8x3VkA@mail.gmail.com>, <F5283140-7DAF-42A6-94F9-22527CF774AA@gmail.com>, <CABCjkDo7d6=V=iRSzbHmACL6xVN-UbCCrASL7ddLTJ7gJJPRzQ@mail.gmail.com>

Dear Jasmin >Perhaps that's what you are referring to by "C-based proof theory such as Simpl". Yes, this is my meaning. I think that this may be a problem in our formalized proof for some algorithm. In the ACL-proof for the Boyer algorithm, the Boyer algorithm is formlized in ACL-functions (or in ACL framework), then it's correctness is proved. However, sometimes we face C-（or JAVA) code for the algorithms directly. We need prove the code's correctness. One way is to translate the codes to Isabelle's framework manually. But this is error-prone. Using a tool mentioned by Jasmin may be better. regards! 2013-08-28 lyj238 发件人： Jasmin Blanchette 发送时间： 2013-08-28 07:20:50 收件人： li yongjian 抄送： isabelle-users 主题： Re: [isabelle] Formally proving the Boyer text matching algorithm Dear Yongjian, I have a further question. If I hace a C code for Boyer text matching algorithm, can I use the C-based proof theory such as Simpl to prove the c-code's correctness? Gerwin Klein's group at NICTA have developed a tool that integrates C with Simpl [1]. Perhaps that's what you are referring to by "C-based proof theory such as Simpl". It should indeed be possible to verify the C code of Boyer-Moore that way. Perhaps those who know the tool better can comment further on its use. Regards, Jasmin [1] http://ssrg.nicta.com.au/software/TS/c-parser/

**References**:**[isabelle] Formally proving the Boyer text matching algorithm***From:*li yongjian

**Re: [isabelle] Formally proving the Boyer text matching algorithm***From:*Jasmin Blanchette

**Re: [isabelle] Formally proving the Boyer text matching algorithm***From:*li yongjian

- Previous by Date: Re: [isabelle] Formally proving the Boyer text matching algorithm
- Next by Date: [isabelle] Localized Named Theorems
- Previous by Thread: Re: [isabelle] Formally proving the Boyer text matching algorithm
- Next by Thread: [isabelle] Localized Named Theorems
- Cl-isabelle-users August 2013 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