模型驱动的分治并行函数式程序生成及自动验证方法

作     者：王忠文 

作者单位：江西师范大学 

学位级别：硕士

导师姓名：王昌晶

授予年度：2023年

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：模型驱动 分治并行 函数式程序 程序生成 自动验证 

摘      要：随着大数据和人工智能的发展,分治并行作为一种通用并行计算框架日益受到重视,它是提高多核资源利用率和执行效率最有潜力的途径。函数式编程作为当前最流行的编程模式之一,在算法领域中有命令式编程不可比拟的优点。函数式程序由于具有强的数学表达性更易于验证,由于具有透明性更易于支持并行计算。然而,目前复杂算法问题的分治并行函数式程序生成是一个难题,采用传统手工证明方法对其验证,不仅易错,且可信度低。针对以上挑战,融合形式化方法,提出了一种基于模型驱动的分治并行函数式程序生成及自动验证方法。首先,从问题描述出发得到功能规约,利用分划递推法和循环不变式开发新策略推导出用Radl语言描述的串行算法;通过对循环不变式扩展与归纳推导出相应的辅助函数和算法连接函数,将串行算法提升为并行算法,使用我们提出的并行算法设计语言Radl对其进行描述;进而,在Isabelle中根据我们提出的用区域定义的同态定理统一验证框架,验证算法连接函数满足同态定理,即提升后的算法可并行化;最后,提出了“Radl→Haskell转换规则,基于此规则设计了“Radl→Haskell并行程序生成系统软件原型,将并行算法转换为Haskell并行函数式可执行程序,且通过GHC平台进行加速比实验。实验结果表明,本文能够生成和验证数组最小和、多项式求值和最大基因序列等一系列算法的并行函数式程序,且具有可解释性和良好加速比。自动验证减少了传统手工验证易错性和繁琐的工作量,保证了算法正确性,对大幅度提升高可信并行函数式程序的开发效率具有重要意义。