程序理论是研究程序的语义性质和程序的设计及开发方法的理论。主要包括程序语义理论、数据类型理论、程序逻辑理论、程序验证理论、并发程序设计理论和混合程序设计理论。程序理论和计算理论是计算机科学的两大支柱。

程序理论的基本问题是如何建立一个相对完善的理论框架，为软件的设计和开发方法提供理论依据。这个框架应能提供有效地描述程序规约的语言；应能定义可操作的变换方法以便能规约构造可执行的程序；应能给出验证程序与其规约之间一致性的机制。

程序语义理论

程序是用程序语言编写的，研究程序的规约、变换和验证，必须首先给出程序语言的语义。这种语义用数学方法刻画程序语句的加工过程，并将其执行结果形式化。所以，程序语义也叫形式语义。形式语义描述技术的本质是用严格的数学方法来研究程序。形式语义的研究始于20世纪60年代初期，ALGOL60 是第一个明确区分语法和语义的程序设计语言。J. McCarthyP. J.Landin，C.Strachy，D. ScottC. A. R. Hoare 和 E. W.Dijkstra 等学者，以及爱丁堡大学和维也纳 IBM 研究中心的计算机科学家们对程序语义的研究和发展都起过重要作用。程序语言的形式语义分为四类: 操作语义 ，模拟程序执行中计算系统的操作过程。指称语义，把程序作为论域间的泛函以便刻画程序的执行数学结果。公理语义，用公理化方法刻画程序与被加工数据的逻辑关系。代数语义，把程序执行的结果定义为满足某种公理体系的代数结构。程序理论对形式语义的需求，促进了论域、偏序以及范畴论等数学理论的发展;而形式语义理论的研究又促进了程序语言和程序设计方法的进步，例如: 在高级语言中广泛使用的过程说明和过程调用的精确概念和实现机制，就是在语义理论的研究中逐步明确的。

并发程序设计理论

20世70年代初期，为了保证在操作系统中多个并行执行进程的正确性，导致了并发程序理论的产生。进入80年代以来，随着超大规模集成电路技术的日臻成熟，并行和分布计算机系统得到了迅速发展，特别是互联网的出现和广泛使用，大大促进了并行程序理论的发展， 使之成为程序理论的一个重要分支。并发程序是包含多个没有因果关系的进程的程序。进程间的通信、同步和它们的并行执行是并发程序区别于顺序程序的基本操作。计算机科学中的并发概念是由Petri 在1962 年提出的。Hoare 和Milner在20世纪70年代后期，分别提出并发程序的CCS和CSP 模型，他们把输入输出以及并行执行作为基本语法成分引入程序设计语言，并使用结构操作语义方法定义模型中基本语法成分的操作语义，开创了用代数方法研究并发程序中通信和并行行为的领域。并发程序理论研究的内容包括: 如何刻画并行进程的行为，在什么情况下它们可以互相模拟，研究各种通信及同步机制，以及死锁及活性，可观察性和发散性等并发现象。并发程序理论的研究加深了人们对并发系统的认识;其主要研究成果，例如， 关于通信和同步的概念，已作为基本语言成分在Ada，Occam和Java等程序语言中得到广泛应用。

混合程序设计理论

进入20 世纪90年代，对控制系统的研究，例如对自动导航及核电站监测等控制系统的研究，引起了程序理论界的关注。这些系统的特点是: 它们都使用计算机进行实时控制; 对控制系统的安全性和可靠性要求高，控制系统的微小错误都将给经济和社会安全带来巨大的损失；系统中都存在两类不同对象：根据传统控制理论，使用微分方程刻画的连续现象和根据逻辑或代数方法， 使用计算机程序控制的离散型事件。这类系统又叫混合系统。混合系统的程序理论已成为研究热点。其基本目标是: 建立混合系统的计算模型，设计描述混合系统的高级语言，探索混合系统程序的设计和开发方法。在建立混合计算模型方面有三种不同的方法: 第一种称为逻辑型混合计算模型方法，其基本思想是在时态逻辑基础上引入时段和切变的概念。时段用于刻画系统在时间区间上的连续变化，切变则表示系统中离散事件间的时序关系。第二种是程序设计型混合模型方法，其目标是在CSP及ADA 等并发语言中引入连续变量及给定初值的微分方程 ，而语言中原有的通信、顺序及条件语句则用来表示系统中离散事件的关系。第三种方法是将自动机概念推广，把微分方程刻画的连续现象扩充为自动机的状态， 用自动机状态转移刻画离散事件间的关系。尽管混合系统理论发展的历史不长， 但它在一些重要的实时控制系统中已经得到了应用，显示出这些理论的生命力。

程序逻辑

程序逻辑是描述和论证程序行为的逻辑，又称霍尔逻辑。程序和逻辑有着本质的联系。如果把程序看成一个执行过程，程序逻辑的基本方法是先给出建立程序和逻辑间联系的形式化方法，然后建立程序逻辑系统，并在此系统中研究程序的各种性质。用逻辑公式描述对输入和输出信息的要求，就可以建立逻辑公式和程序间的联系，表示为

其中P和Q为有关程序变元的逻辑表达式；P称为S的前置条件；Q称为S的后置条件。此公式表示:如果程序S执行前程序变量的值满足前置条件P，且程序S终止，则程序S执行终止后，程序变量的值满足后置条件Q。如果进一步建立一套关于这类公式的推理规则，就能得到一个描述程序行为的逻辑系统，可以在此系统中研究程序的性质，这就是程序逻辑。　程序是在机器中执行的，程序中每个语句的执行导致机器状态的变化，因此程序的执行又可以由机器状态变化的序列表达。数理逻辑中的模态逻辑正是描述动态变元变化的一种逻辑，因此以模态逻辑为基础也可揭示逻辑与程序间的深刻联系。

霍尔逻辑的缺点是其基本形式不能进行逻辑演算。为了克服这种缺点，人们20世纪80年代，提出了类型论方法以求为程序的设计和开发建立更完善的理论框架。比较典型的类型 理论是由P. Martin-L f 建立的，称为直觉主义类型论。它的基本思想是：精选一组类型(集合)作为程序规约，而它们的元素就是满足规约的程序；用一组规则定义类型与其元素间的隶属关系，这些规则即是从规约产生程序的变换规则，又是一阶(直觉主义) 逻辑的证明规则。因此，只要对给定的规约 (逻辑命题)进行证明，就可以构造出符合此规约的程序。这样，程序规约、变换、验证都寓于对规约的证明之中了。

计算理论（Theory of computation）是数学的一个领域，和计算机有密切关系。其中的理论是现代密码协议、计算机设计和许多应用领域的基础。该领域主要关心三个方面的问题：采用什么计算模型（即形式语言、自动机）；解决哪些是能计算的、哪些是不能计算的（即可计算性理论及算法）；要用多少时间、要用多少存储（即计算复杂性理论）。这三方面的问题可以用一个问题来总括：“计算机的基础能力及限制到什么程度？”

计算理论的“计算”并非指纯粹的算术运算（Calculation），而是指从已知的输入通过算法来获取一个问题的答案（Computation），因此，计算理论属于计算机科学和数学。为了对计算进行严谨的研究，计算机科学家会将计算以数学的方式抽象化，称为计算模型。有几种在使用的计算模型，其中最出名的是图灵机。计算机科学家研究图灵机的原因是它很容易叙述，可以分析，用来证明结果，而且用此模式呈现了许多强而有力的计算模型（引用邱奇－图灵论题）。图灵机有潜在的，数量无限的记忆能力，这似乎是不可能达到的，不过所有图灵机解决的可判定性问题都只需要有限量的记忆能力。因此理论上，任何可以用图灵机解决的（可判定性）问题都只需要有限量的记忆能力。