今天下午，听杜玉越老师讲了一堂课，内容是关于“形式化软件开发方法”的讨论。为不负老师为我们所讲的内容，现将笔记整理如下。方便其他人以及自己参考。
一：软件危机
软件由简单到复杂，由小型到大型。出现了很多在软件开发过程中失败的问题。失败率甚至高达70%左右。这就带来了软件危机。
软件危机主要表现在两个方面：
1：复杂度高
2：维护成本高
二：解决“软件危机”
问题出来了，自然就要去解决。于是，应运而生，出现了两种解决办法：
1：软件工程化 即将软件的开发作为一个工程来开发。比如可以借鉴各行各业工程的经验；软件工程的三要素：方法，工具，过程。
2：软件形式化 在逻辑层面上，以系统化的方法刻画、开发和验证系统。在开发之前，对软件的解决方案进行验证。
三：简述“形式化软件开发方法”
分为三个层次：形式化规格方法、形式化验证方法、逐步求精。
形式化规格方法：用数学语言描述软件期望。将自然语言的矛盾，二义性、含糊性等系统性刻画。具有严格的语义和语法。描述的是“做什么”。
形式化验证方法：验证用户需求是否满足。“形式化规格”之后即进行“形式化验证”。目的是早期发现错误，及时改正，减少修改代价。
逐步求精：将在“形式化规格方法”高度抽象出来的模型，逐步的变为可执行的方法。
四：形式化软件开发方法展望
形式化软件开发方法，是软件自动化的前提。即构造出了软件逻辑，代码可以自动生成。
目前，还不能够进行软件自动化，主要是“逐步求精”阶段的脱节，不能很好的使用。现在，大多数是软件半自动化方法。
来源：ericliu000
声明：本站部分文章及图片转载于互联网，内容版权归原作者所有，如本站任何资料有侵权请您尽早请联系jinwei@zod.com.cn进行处理,非常感谢！