什么是程序逻辑？

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

简介：

Hoare 逻辑(也叫做Floyd–Hoare 逻辑)是英国计算机科学家C. A. R. Hoare开发的形式系统，随后为 Hoare 和其他研究者所精制。它发表于 Hoare 1969年的论文"计算机程序的公理基础"中。这个系统的用途是为了使用严格的数理逻辑推理计算机程序的正确性提供一组逻辑规则。

Hoare 认可 Robert Floyd的早期贡献，他为流程图提供了类似的系统。

Hoare 逻辑的中心特征是Hoare 三元组。这种三元组描述一段代码的执行如何改变计算的状态。Hoare 三元组有如下形式

{P}C{Q}这里的 P 和 Q 是断言而 C 是命令。P 叫做前条件而 Q 叫做后条件。断言是谓词逻辑的公式。这个三元组在直觉上读做: 只要 P 在 C 执行前的状态下成立，则在执行之后 Q 也成立。注意如果 C 不终止，也就没有"之后"了，所以 Q 在根本上可以是任何语句。实际上，你可以选择 Q 为假来表达 C 不终止。

这叫做"部分正确"的。如果 C 终止并且在终止时 Q 是真，则表达式就是"全部正确"的。终止必须被单独证明。

Hoare 逻辑为简单的命令式编程语言的所有构造提供了公理和推理规则。除了给 Hoare 论文中的简单语言的规则，其他语言构造的规则也已经被 Hoare 和很多其他研究者开发出来了。包括并发、过程、goto语句，和指针。

1、结构化程序设计

在结构化程序设计中，任何程序段的编写都基于3种结构：分支结构、循环结构和顺序结构。程序具有明显的模块化特征，每个程序模块具有惟一的出口和入口语句。结构化程序的结构简单清晰，模块化强，描述方式贴近人们习惯的推理式思维方式，因此可读性强。

2、面向对象程序设计

面向对象程序设计方法是尽可能模拟人类的思维方式，使得软件的开发方法与过程尽可能接近人类认识世界、解决现实问题的方法和过程，也即使得描述问题的问题空间与问题的解决方案空间在结构上尽可能一致，把客观世界中的实体抽象为问题域中的对象。

程序设计的分类

1、按照结构性质，有结构化程序设计与非结构化程序设计之分。前者是指具有结构性的程序设计方法与过程。它具有由基本结构构成复杂结构的层次性，后者反之。

2、按照用户的要求，有过程式程序设计与非过程式程序设计之分。前者是指使用过程式程序设计语言的程序设计，后者指非过程式程序设计语言的程序设计。

3、按照程序设计的成分性质，有顺序程序设计、并发程序设计、并行程序设计、分布式程序设计之分。按照程序设计风格，有逻辑式程序设计、函数式程序设计、对象式程序设计之分。

---