论文部分内容阅读
计算机飞速发展,促使用户需求单个程序实现更多功能,导致程序行为及结构复杂化,不利于程序设计及性质验证工作。因此,程序行为及结构优化亟待研究及实现。程序行为及结构优化过程中,创建合理的程序形式化刻画系统是研究程序行为及结构的前提。早期的程序形式化刻画系统大都离散化,由抽象的动作、离散的状态及状态间的转移关系构成,可对程序进行基于状态遍历的计算和推理。遗憾的是,它们无法对程序行为即数据流交换过程进行表示和处理。从形式化的角度出发,数据流交换过程可用多项式系统表示的程序是最基础的一类。在了解程序具体行为及整体结构后,定义及判定程序行为等价是实现行为及结构优化的根本。具有相同行为的程序称为等价。基于最精确的系统等价关系互模拟实现程序等价判定,一方面去掉程序中重复的非确定性分支可实现结构优化,另一方面利用行为简单的分支代替行为复杂的分支可实现行为优化。但是,在大部分程序实际应用中,精确的等价关系显得太过严格,适当的近似不会对程序最终结果产生很大影响。为加强程序间关系的灵活性,可在误差范围内放宽等价限制,提出程序近似互模拟概念,并利用数值计算方法创建带误差且误差可控的近似互模拟计算方法,最终实现程序行为及结构近似优化。立足以上需求,本文围绕程序行为及结构优化这一主旨展开研究。针对数据流交换过程可以用多项式系统表示的程序,根据行为特征将之细分为三类,然后分别建立可描述其数据流交换过程的形式化刻画系统,并利用符号与数值混合计算创建程序互模拟及近似互模拟计算方法,其主要贡献包括:(1)构建了程序数据流交换过程划分规则。针对数据流交换过程可用齐次线性多项式系统描述的一类程序,构建了数据流交换过程与齐次线性多项式系统间转换规则。研究得到齐次线性多项式变迁系统,用于描述此类程序数据流交换过程及结构。提出了程序精确行为等价概念,称之为互模拟。基于齐次线性多项式系统系数矩阵的性质,给出了程序互模拟等价计算方法。同时,在给定的变量取值及误差范围内,建立了带误差且误差可控的近似互模拟定义及计算方法,通过矩阵范数实现了近似过程中实际误差的度量。对于实际误差大于给定误差但不大于两倍的给定误差的程序,通过奇异值分解实现了近似程序的求解。实验证明近似互模拟可实现一类程序行为及结构优化。(2)针对数据流交换过程可用非齐次线性多项式系统描述的一类程序,构建了数据流交换过程与非齐次线性多项式系统间转换规则。研究得到非齐次线性多项式变迁系统,用于描述此类程序数据流交换过程及结构。基于互模拟等价及非齐次线性多项式系统增广矩阵的性质,实现了此类程序互模拟等价判定。在非齐次线性多项式系统中,由于常数项的引入,使得针对齐次线性多项式系统建立的近似方法无法得以沿用。为此,在扩大的变量取值范围及给定误差范围内,为此类程序建立了带误差且误差可控的近似互模拟计算方法,通过矩阵范数实现了实际误差的度量。对于实际误差大于给定误差但不大于两倍给定误差的程序,基于QR分解实现了近似程序的求解。实验表明近似互模拟在优化此类程序行为及结构中可行及有效,且近似程序求解过程比齐次线性多项式变迁系统中相应过程节省时间和空间。(3)针对数据流交换过程可用非线性多项式系统描述的一类程序,构建了数据流交换过程与非线性多项式系统间转换规则。研究了非线性多项式变迁系统,用于描述此类程序数据流交换过程及结构。针对线性多项式变迁系统互模拟判定方法无法沿用的问题,基于吴特征列和Groebner基方法实现非线性多项式变迁系统互模拟等价判定,对比分析发现吴特征列方法更优。同时,针对线性多项式变迁系统近似互模拟均需约束变量取值范围的问题,通过对非线性多项式变迁系统近似关系的分析,在无需给定变量取值范围的前提下,在给定误差范围内建立了带误差且误差可控的近似互模拟概念及计算方法。在此过程中近似关系被描述为一个全局最优化问题,称为Max函数,通过填充函数法处理此函数,实现实际误差度量。对于实际误差大于给定误差但不大于两倍的给定误差的程序,通过近似调整非线性多项式系统对应特征列系统中的初式集合,得到了求解近似程序的方法构想。实验表明近似互模拟计算方法实现了程序行为及结构优化,且非线性多项式变迁系统的描述规则及近似互模拟计算方法对于本文所研究的所有类型程序均通用。综上所述,本文以程序行为及结构优化为目标,对可描述程序数据流交换的形式化刻画系统、程序互模拟等价及近似互模拟进行了研究,针对数据流交换过程可用多项式系统表示的程序建立了比较完整的等价及近似理论,为程序行为及结构优化提供了一种形式化的解决思路。