Formal Derivation of Algorithm and Isabelle-based Automatic Verification

摘要

The continuous development of trustworthy software promotes the in-depth study of formal methods. This paper focuses on the formal derivation of algorithm based on recurrence relations. We show two examples of automated transformation processes by combining Isabelle theorem prover with Dijkstra weakest precondition method, that can avoid the error-prone and long-winded problems in manual verification processes. The algorithm formal method that based on recursive relationship can make the derivation process correct through mathematical transformation to ensure the correctness of the algorithm program, as the paper shows.