J.Woodcock&J.Davies_UsingZ_1996_C1 阅读

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的重要性, 给出其主要的功能和贡献, 随后用了一个经典的抽象化, 表现出了形式化和非形式化的区别, 形象地显示了形式化的优势以及可读性.

本文参与腾讯云自媒体分享计划,欢迎正在阅读的你也加入,一起分享。

发表于

我来说两句

0 条评论
登录 后参与评论

相关文章

来自专栏PPV课数据科学社区

数据科学家面试常见的77个问题

[之前翻译的文章,今天看看觉得不错,分享给朋友们!] 随着大数据概念的火热,数据科学家这一职位应时而出,那么成为数据科学家要满足什么条件?或许我们可以从国外的数...

3236
来自专栏AI研习社

深度学习入门指北——从硬件到软件

近日,Rachel Thomas在fast.ai上发布了一篇博文《What you need to do deep learning》,他希望通过这篇文章回答一...

5717
来自专栏奇点大数据

业余时间学数据分析,如何快速上手

数据正在变得越来越常见,小到我们每个人的社交网络、消费信息、运动轨迹……,大到企业的销售、运营数据,产品的生产数据,交通网络数据……

1115
来自专栏数据的力量

如何构建用户画像

3556
来自专栏ATYUN订阅号

【学术】5个字母解释数据科学管道 适合初学者的学习指南

从前,有一个叫“数据”的男孩。在他的一生中,他总是试图弄明白他活下去的目的是什么。比如:“我的价值观是什么? 我能对这个世界产生怎样的影响? 数据从何而来? 我...

3114
来自专栏about云

[干货]如何构建用户画像

从1991年Tim Berners-Lee发明了万维网(World Wide Web)开始,到20年后2011年,互联网真正走向了一个新的里程碑,进入了“大数据...

5128
来自专栏腾讯大数据可视化设计团队的专栏

遇见大数据可视化:来做一个数据可视化报表

上篇文章简单的介绍了数据可视化的基础,将数据进行设计可视化后,可以让我们有一种全新的方式去认识数据,改变对数据的呈现和思考方式。那现在就让我们开始做一份数据的可...

3.1K3
来自专栏大数据文摘

用户画像数据建模方法

3636
来自专栏IT派

从“人人都能编程”到“人人都会研发AI”,苹果低调发布的Create ML潜力无穷

WWDC18上,苹果发布了 macOS Mojave,这版操作系统因为加入了对 iOS App 和黑暗模式的支持而显得尤为重要,但是很多人忽略了苹果面向开发者推...

833
来自专栏EAWorld

边缘计算与云计算的未来

Edge Computing and the Future of the Cloud

5774

扫码关注云+社区

领取腾讯云代金券