超长整数运算的PVS规范与验证

超长整数的运算是现代密码系统的应用基础,运算的正确性关系到密码系统的应用价值。为了验证超长整数算法的设计与需求目标之间的一致性,利用原型验证工具PVS对算法的正确性进行了证明。在介绍了超长整数的加法和减法算法并分析了其设计思想之后,给出了超长整数及其算法的形式规范,通过把算法需要满足的性质描述为定理,将算法的一致性验证问题转化为逻辑定理证明的问题,在PVS定理证明器上完成了相关定理的证明,从而表明这些算法是满足设计需求的。