2023年7月28日发(作者：)

程序设计⽅法和程序分析1.概述

程序设计⽅法和程序分析是两个不同范围应⽤的技术。程序设计⽅法是提⾼程序效率和确保程序正确性⽽产⽣的软件理论。经过战胜软件危机，丰富深刻的设计⽅法的出现，越来越多的应⽤编程，程序员和编程爱好者建⽴了程序设计⽅法学。⽽程序分析是发现程序设计⽅法不能阻⽌的程序错误和程序缺陷⽽发展的。程序分析对已有程序的执⾏次数、程序路径、变量值进⾏分析。

程序效率表⽰程序的性能，⼈们⽤算法复杂度表⽰--理论上的运⾏时间和运⾏所需存储空间，包括程序地址空间和系统栈空间。程序正确性引导程序开发过程，则形成程序的形式推导⽅法。正确性的程序经过正确的程序变换规则⽣成的程序也是正确的。程序正确性能引导程序开发过程。Floyd-Hoare规范公理⽤短⼩精悍的不等式、数学表达式和逻辑运算符表⽰前断⾔P和计算语句结果的后断⾔Q，控制条件B划分为{B,-B}成为条件语句P或循环语句Q的⼀部分。验证的形式是规则前提和结论的分式形式。 程序效率在结构程序设计上，表现的特征是单⼊⼝和单出⼝的相对独⽴的控制语句，因此循环语句可视为单路径⽽if-else条件语句则是双路径；程序正确性则表现为程序具体结构和内部逻辑的良型控制结构。过程则对时间⼀定有要求。Unix/Linux系统的并发程序或多核多线程必须处理程序实体在执⾏时间上的严格性要求，所以应建⽴进程(线程)调度的合乎运⾏机制的时间序列，以防⽌死锁、进程实际饥饿和资源消耗。程序效率则表现在进程控制语句fork()、waitpid()、signal()、exit()、ftok()和msgget()等对进程创建和执⾏时间与进程间关系的精确控制和进程存储空间的管理，程序正确性则是并发程序能遵循进程(线程)调度和执⾏的全部正确性原则。程序效率在⾯向对象技术上，表现的特征是类、模板封装的内聚性和实现的独⽴性，⽽且实例化和类对象的存储管理也是特征。⽽效率的另⼀个特征是软件复⽤，类库与过程式函数库调⽤复⽤相似，STL的容器和模板的实参具有数据类型的通⽤⽅式的实例复⽤，类层次的继承是软件复⽤的进化。此外，多态是函数参数数据类型的多种形式的要求，可认为是currying技术的应⽤[4]。程序正确性在⾯向对象技术中的应⽤表现在四个⽅⾯：(1)设置访问控制，类、继承和友元的访问权限，（2）独⽴设计⽅法：类的接⼝与实现分离、虚拟函数与继承实现、模板定义与实例化、容器与元素实参数据类型(并不熟练)（3）管理存储单元：静态成员、对象、容器、多继承，防⽌资源重复删除和悬挂指针。（4）最后是系统⾃动调⽤的机制。系统⾃动调⽤创建、复制构造、赋值、移动、析构操作和实现默认类操作，防⽌对类和对象的活动期管理出现漏洞。Backus在1977年的图灵奖颁奖典礼上发表的演讲提出函数式FR程序设计。⽤⽆变量的原始函数的递推公式定义、函数组合和泛函型的⽅法编程，主要使⽤递推公式映射的递归⽅式，程序代数可实现FR推导。现代函数式程序的效率表现在⽤运⾏时系统的图规约表⽰⾼阶函数和惰性计算。程序正确性表现在可计算函数和数学泛函型的正确性上。FR函数程序设计反应了输⼊数据和输出数据间的关系(Relation)，也可⽤传递函数实现，因此前后断⾔和谓词转换器能证明程序正确性。但是Relation不是流程，⽽是组成程序执⾏过程的操作有序组。Lisp和prolog是⼈⼯智能推出的逻辑式程序设计，是在解空间事实和规则的⼦句列表推理执⾏(寻找与合⼀)“新”事实的⽅法。实际上，逻辑式程序设计中的关系，并不是⾼阶函数或者传递函数，⽽是多个项间的关系或约束。

编译原理使⽤程序分析⽅法，包括控制流、数据流、符号分析，⽬的是发现控制流⾛向，优化程序，产⽣⽬标代码，以及分析并⾏成分。程序设计⽅法和程序分析的关键技术有：（1）实例化，原因是程序分析中数据与变量的相对独⽴性，程序设计⽅法中类型与类型名的独⽴性，操作对象与具体数据结构实现的相对独⽴性。（2）映射，包括数据类型的数据实例化，C++的map类，类模板实参，多态函数在运⾏时绑定，甚⾄包括递归程序的取样规则和展开规则，⽽程序变换的等价模式有序对也可看作映射，尽管需要程序变换规则。（3）软件复⽤，库函数、封装、模板和容器、数据结构的通⽤算法。程序设计⽅法和程序分析关键技术见表1，分类表⽬包括1和2类，分别是程序设计⽅法和程序分析两种类型。表1 程序设计⽅法和程序分析的关键技术 功能需求程序执⾏过程构造基础理论基础分类程序形式推导函数式程序不变式,界函数，⼀阶谓词⽆变量函数定义与组合型 语句，⾯向⽬标。最弱前置条件1图规约语句，函数与泛函型程序变换和程序代数1程序变换程序形式规范 ⼀阶谓词与函数定义程序变换规则1ADT代数规范(操作)公理⽤作程序符号执⾏树类(class)抽象代数1符号执⾏部分值求解 路径约束程序形式推导2静态精确公式，动态转换系统*程序例化器程序、输⼊数据，例化程序程序转换与程序例化。s-m-n理论编译原理2控制流图数据流图程序切⽚Floy-Hoare最弱前置条件程序测试CFG* 基本块2DFG* 变量依赖编译原理2FG,PDG,SDG* 语句，可达信息流和路径例化规则与证明2{P}S{R}前后断⾔语句，上下⽂1wp(“S”,R) 语句，谓词转换器谓词语义1路径，循环*测试⽤例 1,2 在表1可知，程序的功能需求表⽰在程序设计中，⽤程序形式规范，实质是⼀阶谓词（若不包括程序分析中的程序结构⽅式*），Floyd-Hore规则逻辑和wp(“S”,R)谓词转换器的实质也是⼀阶谓词或者功能相似的数学表达式。另⼀种表⽰形式是代数规范或者泛函数型。因此对程序功能的表⽰是不⾜的，谓词和不等式并不能刻画程序功能的实质。程序功能是表⽰程序对数据的操作，例如复制移动、计算、排序、路径节点的集合扩展，以及数据间的逻辑关系，例如follow集、first集、R[com]算法的计算关系、数量⼤⼩关系和路径关系，实现程序的外在功能。