程序设计理论
程序设计理论
programming theory
研究程序设计的理论基础、基本原则和一般方法的一种理论。是计算机软件工程学的基础。程序设计的基本过程是：对待解决的问题进行分析，定义用户需求，描述数据和加工过程，再把这种描述细化、编码，转换成计算机可以接受的表示形式。
自20世纪40年代带内存程序的计算机诞生后，计算机编写程序的工作越来越重要。到60年代中期，计算机应用已相当普遍，但软件设计技术却很落后，许多大型软件的质量低劣，可靠性不高，可维护性极差；软件生产率很低，从而价格昂贵，供不应求，造成所谓的软件危机。计算机科学家开始认真研究程序设计的基本理论和方法。60年代末期，结构化程序设计与自顶向下逐步求精的原则和方法受到广泛重视。结构化程序设计希望通过完善程序的静态结构来保证程序动态运行的正确性，因而需要限制或取消某些不良程序语句，例如GOTO语句。自顶向下逐步求精的主要思想是从待解问题出发，运用科学抽象的方法，把原问题分解成若干相对独立的小问题，依次细分，直至各个小问题都获得圆满解决为止。
与此同时，使用逻辑方法验证程序正确性的研究取得了丰硕成果，形式语义学也得到长足的进展。验证框图程序的断言方法是在框图的每条边上附上一个断言（谓词公式），其意义是，每当程序运行到达这条边时，此断言应为真。对于循环，即框图上的一个回路，可以定义一个断点，并在断点上设置一个断言ρ，然后证明若循环开始时断点上的ρ为真，则当循环返回到该断点时ρ仍然为真。断言ρ常称为循环不变式。Hoare逻辑是基于上述断言方法的程序验证系统，它是一阶谓词逻辑的扩充，用于证明程序的部分正确性。形式语义学是程序设计理论的主要组成部分。70年代程序设计理论研究的主要课题是大型程序的设计方法。对于复杂而庞大的大型程序设计，原先的简单类型、子程序、过程等概念已显不足，需要一种表示能力更强、更灵活、结构更清晰的程序单位，这就是抽象数据类型。抽象数据类型把模块概念精确化和理论化，成为程序设计理论中的重要组成部分。
70年代中期以后，程序设计理论朝多方向发展。第一，对程序设计的范型进行研究。最主要的程序设计范型有：逻辑式程序设计，函数式程序设计，面向对象的程序设计。第二，软件生产自动化研究。这种研究的主要目的是希望能像工业生产自动化那样，使程序设计的某些过程实现自动化，从而提高软件生产率，保证程序正确性。这方面研究的主要成果是形式化软件开发方法，其目标是为使用者提供一整套思维方法和描述、开发手段，如规范描述的原则、程序开发的一般过程、描述语言等等，使开发者能利用数学概念和表示方法恰当合理地构造形式规范，根据开发过程的框架及设计原则进行规范描述和系统化的设计精化，并使用证明的概念对规范的性质和设计步骤进行分析和验证。第三，发展新应用领域中的程序设计理论与方法，例如并行程序设计，实时程序设计，混杂系统的程序设计等等。