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 |
程序变换 |
程序形式规范 |
|
一阶谓词与函数定义 |
程序变换规则 |
1 |
ADT |
代数规范(操作) |
公理用作程序 |
类(class) |
抽象代数 |
1 |
符号执行 |
|
符号执行树 |
路径约束 |
程序形式推导 |
2 |
部分值求解 |
静态精确公式，动态转换系统* |
程序例化器 |
程序、输入数据，例化程序 |
程序转换与程序例化。s-m-n理论 |
2 |
控制流图 |
CFG* |
|
基本块 |
编译原理 |
2 |
数据流图 |
DFG* |
|
变量依赖 |
编译原理 |
2 |
程序切片 |
FG,PDG,SDG* |
|
语句，可达 |
信息流和路径例化 |
2 |
Floy-Hoare |
{P}S{R} |
前后断言 |
语句，上下文 |
规则与证明 |
1 |
最弱前置条件 |
wp(“S”,R) |
|
语句，谓词转换器 |
谓词语义 |
1 |
程序测试 |
路径，循环* |
测试用例 |
|
|
1,2 |
在表1可知，程序的功能需求表示在程序设计中，用程序形式规范，实质是一阶谓词（若不包括程序分析中的程序结构方式*），Floyd-Hore规则逻辑和wp(“S”,R)谓词转换器的实质也是一阶谓词或者功能相似的数学表达式。另一种表示形式是代数规范或者泛函数型。因此对程序功能的表示是不足的，谓词和不等式并不能刻画程序功能的实质。程序功能是表示程序对数据的操作，例如复制移动、计算、排序、路径节点的集合扩展，以及数据间的逻辑关系，例如follow集、first集、R[com]算法的计算关系、数量大小关系和路径关系，实现程序的外在功能。