前言
TLA+ in practice 学习笔记前段时间看到一篇文章,是讲AMS使用TLV+来测试其开发的系统,文章中讲TLA+是一种容易学习和掌握的形式化语言。为此,我从网上找到了一本Practical TLA的书,阅读之后,还是有一些心得。
这本书,是一本使用TLS进行设计验证的入门书,TLA是很晦涩的,为了便于使用,作者又开发了一门基于TLS的DSL语言–PlusCal。PlusCal是一门具有函数式编程风格的描述语言,虽然对于C语言程序员而言仍然不容易掌握,但是相对于TLA来说已经是好了很多的了。
那么,这本书,按照作者的说法,希望对读者有两方面的帮助:
首先就是对模型进行检查。模型是对现实世界事物的一种理想化的抽象,在建模的过程中,会强迫设计者识别哪些是重要的概念,哪些是不重要的概念。在这本书中,时时刻刻体现了模型的概念。
其次,是
第一个例子
第1章 一个例子1.1 问题域银行,Alice和Bob是两个用户,银行提供了在线转帐的业务(wire":
每个转帐业务只在不同的两个银行客户之间进行,转帐金额最少一美元
若成功了,金额会从转出者的帐户减去,并加到转入者帐户上
若失败,两个账户都不受影响
不能让帐上金额为负
多个转帐可以同时进行
1.1.1 代码框架ToolBox
1.2.2 定义规格两件事要定义:人(帐户)的集合,以及每个帐号的金额
在variables中定义变量
在define区域中定义不变量
1234567891011121314151617EXTENDS Integers (*--algorithm wire variables people = {”alice“, ”bob“}, acc = [p \in people |-> 5], sender = ”alice“, receiver = ”bob“, amount = 3; define NoOverdrafts == \A p ...