J.Woodcock&J.Davies_UsingZ_1996_C1 阅读

文章概要

随着软件的日益发展, 软件的功能等需求越来越多, 文档也随之增加, 组件之间的交互和冲突最后导致系统出现问题, 逐渐偏离了我们的预期. 为解决该问题, 其中一个重要的方法就是形式化.

虽然在软件生命周期之中, 我们有许多文档, 涵盖大量的图片, 文字和图表, 但是这些都是模糊不清的, 重要的信息都被隐藏在不相干的细节之中, 缺陷发现的过于迟, 进而导致严重的问题. 形式化解决了该问题, 它可以产出精确的, 非模糊的文档, 并且该文档可以用于设计阶段, 以及作为后续的开发, 测试和维护作为导向.

虽然形式化十分有用, 但是其数学基础是和通常的数学不太一样的, 因此使用它的成本是较为高昂的, 但是不可否认的是, 形式化的的确确可以减少最终的耗费.

CICS是世界上大多数成功的软件之中的一个, 它是一个信息管理系统, 并且被广泛地使用在各个领域, 开发之后的10年, 软件变得十分复杂, 提出来一个解决方案是, 找到一个更为精确的方法来确定功能, 而这样的精确就需要使用数学技术. Kenny和Hoare尝试解决这个问题, 引出了Z符号, 利用该方法来对CICS确定新的功能, 这种方法易于学习和使用, 即使使用者没有任何数学的预备知识.

Z notation是基于集合论和数学逻辑的, Z notation使得其数学形式是结构化的, 由声明和约束构成的模式, 这样的语言可以用来表述一个系统的状态, 属性等, 重要的是, 可以用该方法来改良原有的设计. 另外, Z notation使用自然语言进行表述, 对于读者来说阅读起来十分轻松. 数学语言加上强大的结构化技术, 最终可以产出形式化的规格说明书, 可以使用数学逻辑的验证技术来对这些说明书进行推断. Z并不是用于非功能属性的描述, 比如可用性, 大小, 性能和可依靠性.

构造证明的过程可以帮助我们更好地理解系统的需求, 帮助我们找到那些隐藏的假设, 在规格说明书上的证明对于软件质量来说至关重要.

阅读感悟

该文章很好地梳理了Z notation的起源. 从软件的开发谈起, 引用CICS的开发历程, 引出了Z notation, 阐述了Z notation的各方面的优点以及其特有的性质, 又说明了在Z notation之中Proof的重要性, 给出其主要的功能和贡献, 随后用了一个经典的抽象化, 表现出了形式化和非形式化的区别, 形象地显示了形式化的优势以及可读性.