一种适用于形式化验证的智能合约编译方法

摘要

本发明公开了一种适用于形式化验证的智能合约编译方法，提出的一种新型智能合约编译语言，其包含工程应用和类型数学集合，利用形式化证明结合语言编辑，可在运行前发现所有的Bug，能保证所写程序安全无漏洞并且操作简单的编辑语言，实现智能合约形式化验证实时进行；在进行合约形式化验证时，本发明仅需对所使用函数定理进行证明，无需函数建模，大大提高了智能合约编译效率。