聊聊 Formal Specification, 举个验证并发的例子

在 17 年 11月 20日那篇文章中,拉开了 TLA+ 的序幕。终于从无到有,了解了 TLA+ 的面貌。

但对于 TLA+ 真正的威力,前一篇文章,并没有感性的认识。在学习的过程中,找到了一个网上比较好的例子,可以 帮助对 TLA+ 有更深入的理解,例子摘自 Learn TLA+ 网站


在交易系统中,转账是最为常见的业务需求。

设想有这样一个普遍场景,甲的账户有 10元,乙账户有 10元,此时甲将 5元转至乙账户,那么甲账户金额变为 5元,乙账户金额变为 15元,转账完成。

但是,事情往往并没有我们所想象的那么简单。

阅读更多

聊聊 Formal Specification, 从 TLA+ 讲起

第一次听到 TLA+ 是自大丰哥与德国慕尼黑参加数据库大会时,听了 Microsoft 所做汇报时,了解到的。处于大家对此新生事物的好奇,他遍将此作为一项课题,安排于我,因此有幸对 TLA+ 做进一步的研究。
在研究过程中,随着对 TLA+ 的了解的逐步加深,我见识到了 Formal Specification (以下简称 Spec)这个更为广阔的领域。
Spec 是一个有着半个世纪历史的研究领域,自从大型机时代,便有了其雏形。那时的软件开发手段并不如现在那样丰富,也缺乏系统性的理论知道,数学家、计算机科学家等致力于为软件系统开发提供更为安全、可靠、HA 的软件系统,在此摸索过程中,遍诞生了 Spec 这的研究。

阅读更多