形式化解决了该问题, 它可以产出精确的, 非模糊的文档, 并且该文档可以用于设计阶段, 以及作为后续的开发, 测试和维护作为导向....Kenny和Hoare尝试解决这个问题, 引出了Z符号, 利用该方法来对CICS确定新的功能, 这种方法易于学习和使用, 即使使用者没有任何数学的预备知识....数学语言加上强大的结构化技术, 最终可以产出形式化的规格说明书, 可以使用数学逻辑的验证技术来对这些说明书进行推断. Z并不是用于非功能属性的描述, 比如可用性, 大小, 性能和可依靠性....构造证明的过程可以帮助我们更好地理解系统的需求, 帮助我们找到那些隐藏的假设, 在规格说明书上的证明对于软件质量来说至关重要.
阅读感悟
该文章很好地梳理了Z notation的起源....从软件的开发谈起, 引用CICS的开发历程, 引出了Z notation, 阐述了Z notation的各方面的优点以及其特有的性质, 又说明了在Z notation之中Proof的重要性, 给出其主要的功能和贡献