Re: [isabelle] Formally proving the Boyer text matching algorithm



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/


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