软件函数形式语义及形式化证明脚本自动生成方法

摘要

本发明公开了一种软件函数形式语义及形式化证明脚本自动生成方法，包括：对汇编指令执行后的新系统状态进行构建，使经过指令执行后的新系统状态的每个状态分量均由初始系统状态的状态分量表示；构建所有汇编指令的形式语义函数库；记录在构建被改变状态分量值的表达式树用到的指令语义函数和子路径语义函数，以及表达式化简中用到的化简规则和子路径语义证明定理，自动生成指令执行后新状态的形式语义和相应的形式化证明脚本。本发明能够对输入的微内核操作系统中的一个函数生成汇编代码、生成该汇编代码对应的若干条执行路径信息、对每条执行路径生成相应的形式语义和形式化证明脚本，最终生成自动生成函数的形式语义和形式化证明脚本。