随着软件的日益发展, 软件的功能等需求越来越多, 文档也随之增加, 组件之间的交互和冲突最后导致系统出现问题, 逐渐偏离了我们的预期. 为解决该问题, 其中一个重要的方法就是形式化.
虽然在软件生命周期之中, 我们有许多文档, 涵盖大量的图片, 文字和图表, 但是这些都是模糊不清的, 重要的信息都被隐藏在不相干的细节之中, 缺陷发现的过于迟, 进而导致严重的问题. 形式化解决了该问题, 它可以产出精确的, 非模糊的文档, 并且该文档可以用于设计阶段, 以及作为后续的开发, 测试和维护作为导向.
虽然形式化十分有用, 但是其数学基础是和通常的数学不太一样的, 因此使用它的成本是较为高昂的, 但是不可否认的是, 形式化的的确确可以减少最终的耗费.
CICS是世界上大多数成功的软件之中的一个, 它是一个信息管理系统, 并且被广泛地使用在各个领域, 开发之后的10年, 软件变得十分复杂, 提出来一个解决方案是, 找到一个更为精确的方法来确定功能, 而这样的精确就需要使用数学技术. Kenny和Hoare尝试解决这个问题, 引出了Z符号, 利用该方法来对CICS确定新的功能, 这种方法易于学习和使用, 即使使用者没有任何数学的预备知识.
Z notation是基于集合论和数学逻辑的, Z notation使得其数学形式是结构化的, 由声明和约束构成的模式, 这样的语言可以用来表述一个系统的状态, 属性等, 重要的是, 可以用该方法来改良原有的设计. 另外, Z notation使用自然语言进行表述, 对于读者来说阅读起来十分轻松. 数学语言加上强大的结构化技术, 最终可以产出形式化的规格说明书, 可以使用数学逻辑的验证技术来对这些说明书进行推断. Z并不是用于非功能属性的描述, 比如可用性, 大小, 性能和可依靠性.
构造证明的过程可以帮助我们更好地理解系统的需求, 帮助我们找到那些隐藏的假设, 在规格说明书上的证明对于软件质量来说至关重要.
该文章很好地梳理了Z notation的起源. 从软件的开发谈起, 引用CICS的开发历程, 引出了Z notation, 阐述了Z notation的各方面的优点以及其特有的性质, 又说明了在Z notation之中Proof的重要性, 给出其主要的功能和贡献, 随后用了一个经典的抽象化, 表现出了形式化和非形式化的区别, 形象地显示了形式化的优势以及可读性.