Re: [isabelle] Formally proving the Boyer text matching algorithm
>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.
发件人： Jasmin Blanchette
发送时间： 2013-08-28 07:20:50
收件人： li yongjian
主题： Re: [isabelle] Formally proving the Boyer text matching algorithm
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 . 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and