区块链智能合约形式化验证代码转换器及转换方法

摘要

本发明公开了区块链智能合约形式化验证代码转换器及方法，将多种语言开发的智能合约程序代码自动化转换为形式化验证辅助证明器可识别运行的中间层语言M+代码，然后通过形式化验证辅助证明器对工具生成的中间语言M+语言代码进行自动化安全验证，高自动化的将智能合约源代码一键转换为形式化验证中间语言M+代码，自动提取形式化代码中的数据类型、运算符、特殊结构、条件和循环语句、函数继承关系、函数限定符等内容，并映射到执行空间执行，从而极大程度的提高区块链智能合约形式化安全验证效率，减少了人工参与度，提高了自动化程度，同时也确保了代码形式化过程的准确性。