瀑布模型是将软件生存周期的各项活动规定为按固定顺序而连接的若干阶段工作，形如瀑布流水，最终得到软件产品。它在1970年由温斯顿·罗伊斯（Winston Royce）提出，直到80年代早期，它一直是唯一被广泛采用的软件开发模型。
本书中例出了瀑布模型的文档图，但是鄙人并没有看得很懂它的用意。
搜索一些关于瀑布模型的解释后看到了这样一句话：”瀑布模型的本质是‘一次通过’；它是一种文档驱动模型，在可运行产品交付之前，客户只能通过文档来了解最终的产品会是什么样子。“
这才恍然大悟书中那个8种文档被各个过程生产、修改的含义。由于瀑布模型是线性的，在最终产品产生前，如何产生有用的文档指导开发、衔接两个阶段非常重要。
形式化方法建立在严格的数学基础上，其目标是希望能使系统具有较高的可信度和正确性，并能使系统具有良好的结构，使其易维护，关键是能较好地满足用户需求。“形式化方法”一词虽然一直被广泛地应用，但在不同程度上，因理解不同，使其具有了不同的含义。一般说来，形式化方法是指具有坚实数学基础的方法，它是数学上的综合、分析技术的应用，用于开发计算机控制的系统，经常有推理工具的支持，它可提供一个用于模型设计和分析的一个严格而有效的途径。
形式符号系统具有一定的数学性质，所以它们非二义性的基础在于其内在的数学结构。越是复杂的数学概念，越是建立在更原始的概念之上，如：集合、命题逻辑。这就是说，形式符号系统可以具有合适的解释，并在理论上足以确保规范的一致性解释。 形式规范是由一些精确的定义组成的，因为其符号系统的含义是明确定义的。相对地，若将英语作为交流媒体，将很难得到精确的规范。精确规范的直接益处在于：它能减少规范中的二义性和误解释的可能性（危险）。精确是形式化方法或形式符号系统的一个特征，是产生无二义性规范的主要依据。另外，形式规范主要的语用益处在于：可以对形式规范进行较详细的构造性检查，因为对此规范中的具体内容的含义不会有争议，有争议的只是内容的完备性。换句话说，精确有助于确认和交流。 由于适当的形式机制的使用，使得规范的抽象性成为可能。抽象是人们处理复杂性的主要智力工具之一，而且通过忽视不感兴趣的部分，从而有助于清晰性。各种形式符号系统对于精确、抽象地表达概念具有各自不同的能力，但它们均可用于严密地描述概念，更重要的是，它们比自然语言的描述更严密、更精确、更抽象。一般地，形式系统（框架）使得表示一个规范与其相应程序之间的映射成为可能。 形式规范有一个很有价值的特性：可操纵性。这就是说，可以在明确定义的规则的指导下，分析规范或或对形式规范进行变换。利用形式规范的可操纵性可以证明规范的一致性；可以推导出关于此规范的一些重要结果；还可以验证规范的实现过程，至少可以验证源代码相对于其规范的正确性。更一般地说，有可能将不同级别规范间的验证以及规范与程序间的验证问题简化为形式证明问题。这样，形式化方法就可以提供程序对应其规范的非常高的可信度。所以，可操纵性也有助于确认，并且由这种特性可以得到进一步的抽象（推导出的性质），同样，也有助于使得规范更清晰。
标签：读后感,模型,形式,规范,形式化,构建,精确,文档 From： https://www.cnblogs.com/baizhuoran/p/18042009