PlusCal
第2章 PlusCal2.1 介绍2.2 定义规格2.2.1 规格的布局
在MODULE前后各至少要有四个-，由至少四个=结尾
模块名必须和文件名相同
EXTENDS导入外部模块，这里导入了Integers
\*是行注释，(* ... *)是TLA的块注释。PlusCal写在TLA的块注释中(这样TLA的解释器会忽略它），并由- -algorithm <name>开始，由algorithm结尾。algorithm的名字不需要和文件名一样
在algorithm中，用variables标示初始化变量，变量之间用,隔开
我们在这里写我们的算法
2.2.2 表达式在TLA中，一切要么是表达式Expressions，要么是操作子operator。
expression evaluator
2.2.3 值基本值类型TLA支持的值类型：string, integer, Boolean, 以及模型值(model value)。不支持浮点数
支持的操作：
注意=和:=的区别：
=是相等比较，:=是赋值
在纯粹的TLA中，只有相等比较，没有赋值。若x已初始化了并想将其与1比较，用x ...
后记
大概是因为安全的事情, 公司安全一下子搞得特别认真.
那天看到一篇亚马逊使用TLA来做形式化验证的文章, 对TLA感兴趣了, 就找到这本入门的书看了一下. 这本书纯粹是一个DSL语言和工具的使用, 实际上并没有牵涉到太多的数学的东西. 只要能看懂函数式语言, 基本上都能够看懂. 但是担心不用就会忘了, 所以当笔记一样把比较重要的东西给翻译了一下.
但是, 这个东西其实还是只适用于算法的验证, 而不是什么业务流程的实现和代码的验证.
后来我们联系了华东师大的一位做形式化设计的著名教授来交流过一次，他参与过上海地铁的软件设计。那个是真的需要形式化来证明软件的正确性。但是了解下来感觉，即使是华为，像我们这种需要7x24x356连续工作的RRU设备，用形式化也太奢侈了。即使是RRU这种相对规模比较小的产品，也超过了80万行代码，根本不可能搞什么形式化。至于人员能力水平就更不要提了，或许只有计算机科学科班出身的才知道这个是什么，像我们这种半路出家的都需要重新学习。
这个东西也就是在华为这种公司有意义，离开了之后，一般的企业根本达不到这个级别。就是屠龙技了。
前言
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 ...