需求文档

我们要建立一个银行系统的模型，它的需求文档如下所示：

说明	标签
这个系统包含账户(account)和人(person)	ENV-1
一个账户有余额(balance)，余额是一个有上限的非负数	ENV-2
一个账户只有一个所有者(owner)，也就是说一个账户对应着唯一的人(person)	ENV-3
账户可以执行开户(open)和销户(close)操作	FUN-1
只有当一个账户的余额为0时，它才能销户	FUN-2
钱可以从账户中取出(withdraw)或者存入(deposited)	FUN-3
钱可以从一个账户转移(transferred)到另一个账户	FUN-4
钱可以从普通账户转到活期储蓄账户	FUN-5

注：国外账户类型有多种，其中一种是普通账户(normal account，也许应该叫checking account?)，没有利息，一种是活期储蓄(saving account)，活期利息

初始建模

初始化不变量

初始的建模就先简单点，我们只考虑环境相关需求以及FUN1至FUN3的内容，之后的内容我们可以通过一步步精化来实现

在建模前我们还是先来小小的分析一下，一个账户对应着唯一的一个人，每一个账户都有一个余额，如果设计一个数据库来存储这三个字段的话，我们肯定会选取account来当主键，因为一个人可能拥有多个账户，而一个账户所对应的人是唯一的。

对应的person和balance我们都通过这个account来取到，在event-b中我们通过全函数（一种集合关系，在定义域中每个值都对应着一个值域中的值）这个概念来实现

在这里插入图片描述
先来实现一下环境相关部分，这部分内容是不会变的，我们建立一个context，随便取个名字叫ct好了

ct里面有：A代表所有账户的集合，P代表所有人的集合，c代表存款的上限（当然现实中应该不需要这玩意儿……），并且有个公理：c必须要大于0

初始化变量

模型不变的部分建立完毕，来构建模型中变化的部分，新建一个machine，叫它mac1

要建立的变量有三个，一个叫account，代表现在存在的账户，它是所有账户A的子集，一个叫owner，代表从账户到人的映射，最后一个叫balance，它代表从账户到余额的映射

rodin中建立变量有简单的方法，点击左上角的"open the new variant wizard"
在这里插入图片描述
然后在框框里填上变量的名字以及初始化

变量名叫account，它是一个集合，初始化为空集，然后不变式一栏里面填写account是A的子集，在这个框框里输入 $\subseteq$ 只要在键盘上输入<:就可以了

在这里插入图片描述
然后是owner，前面说了owner是一个全函数，形式是一个集合，它的样子类似于{account1->person1, account2->person2}，它的初始化也是空集，因为刚开始什么账户都没有，里面的映射也是什么都没有。（ $\rightarrow$ 代表的是全函数，输入 $\rightarrow$ 的方法是“减号减号大于号”–>）
在这里插入图片描述
balance同样是一个全函数，不过它是account账户到0…c这一区间的全函数，0…c是一个区间的意思，相当于{0,0+1,0+2,…,c}

在这里插入图片描述

定义open

完成了变量相关的定义和初始化，之开始定义event

在这里插入图片描述
在事件里面添加一个名叫open的事件，代表开户操作，在开户操作中，我们要做的事情有三件：1、新增一个账户a，将其加入account。2、添加账户到余额的映射，刚开的账户里余额等于0。3、添加账户到人的映射。

我们看到了，要完成这三件事情，需要添加两个变量，分别为账户a以及人p，这个操作我们没有使用过，也是在Event栏目下右键，然后点选Add Event Parameter，将两个变量分别命名为a和p，这样Rodin就会知道完成这个Event需要这俩变量，当然了，guard条件还是要加上的，a不能属于account，因为新建的账户肯定不能是已有的账户，p是一个人，所以要属于P
在这里插入图片描述

定义close

销户操作我们只需要一个account，从需求文档中看到了，执行销户操作时该账户余额必须为0，所以多了一个balance(a)=0的条件

要执行的操作是把这个account从所有先存account集合中删除，account := account \ {a}，这个"\"就是取差集的意思，用来把{a}元素从集合中删除，当然还要顺带着把balance和owner这俩函数中删除a的映射
在这里插入图片描述

定义deposit

存钱操作呢，就是考虑往哪一个账户里面存多少钱，所以需要一个代表账户的a以及代表存多少钱的q，这个存多少的q肯定要大于0，而且这个钱存进去之后不能超过上限c，这里我们就简单地认为如果存入钱后余额超过了c，那么这次存款就不让它存了，嗯，就这么简单
在这里插入图片描述

定义withdraw

在这里插入图片描述
取钱操作和存钱相反，从某个账户中拿钱，一个账户取出钱后余额肯定不能小于0，不然银行肯定要倒闭

额外操作：
这里我们实现一个额外的操作，如果存入钱后余额超过了上限c，那么只让它存到上限c，如果取出的钱大于当前的余额，那么只让它取出全部的余额，其实这俩操作很好实现，只要另外定义俩事件就可以了
在这里插入图片描述

如果上面的操作都是这样一步步完成的话，那么看看左边证明义务里面都是通过的，至此我们完成了初次的建模操作。

第一次精化

在第一次精化中，我们将要实现FUN-4，也就是将钱从一个账户中转到另一个账户，在实现中我们要使用精化的思想来实现这一功能，将转账这一过程通过继承之前已经实现过的deposit和withdraw这俩事件来完成（啥？你说再定义个事件就OK了？当然这样也可以，不过这里为了展示精化的思想，我们还是强行用一下精化）

好的，我们重新来考虑一下我们的需求

钱可以从一个账户转移(transferred)到另一个账户

我们设计了一个如下的架构，一个转账的操作分为两个步骤，第一个步骤是将钱从账户扣除，并且将转账的金额和转账的目的记录，金额记为q，目标账户称为a，而记录称为t好了，第二步是根据t里面的信息从目标账户a存钱，存入的数量为q

一个操作是取钱，一个操作是存钱，新的事件称为transfor_1和transfor_2，在这里我们可以用上Event-B的精化机制，让事件transfor_1和transfor_2分别继承withdraw和deposit

至于这个记录，我们采用的形式是t --> <q,a>，也就说是，将t作为主键，知道t就可以取到<q,a>这个有序对
在这里插入图片描述
开始构建模型

在ct上右键选择extend，就是继承，新的context就叫ct1好了
在这里插入图片描述
看到继承后，之前版本的内容会被隐去，专注于新变量就行，和代码的继承功能差不多

在ct1里面我们要定义一个T，它代表所有转换事务的集合
在这里插入图片描述
在mac1上点一下refine（精化），和继承差不多的意思

看到refines和sees里面都有了对应的内容，点击mac1和ct1可以修改精化和观看的内容，不过改完后可能不会马上有反应，这时候请按一下F5刷新一下下

这里精化之前的内容都用浅绿色标出，而新添加的内容就是原来的深绿色

按照刚刚的分析，我们来添加一下trans这个变量以及aq_of_trans这个函数

注意到aq_of_trans这个函数的写法，因为是trans对应<account, quantity>这个有序对，所以这里用了x这个笛卡尔积的符
在这里插入图片描述
加入两个新的Event，点击添加事件的精化

让transfor_1精化withdraw，让transfor_2精化deposit

接下来只要按照刚刚设计的思路写下去就可以了，transfor_1好像没啥难的，条件也清除，就是act3这里 $aq\_of\_trans := aq\_of\_trans \cup \{ t\mapsto(b\mapsto q) \}$ ，这里第一个 $\mapsto$ 表示的函数的映射，虽然表示映射的方式用了有序对，第二个 $\mapsto$ 单纯表示的是有序对
在这里插入图片描述
transfor_2这里有序对的取值函数是prj1和prj2，就是分别取有序对的第一个值和第二个值，我也是在手册上翻了好久才翻到的

在抽象的事件上的a和q，现在我们可以用更加具体的值来取代，所以这里要用上with语句，也就是把a的值用prj1(aq_of_trans(t))取代，q的值用prj2(aq_of_trans(t))取代。其他的条件其实完全没变化，就是替换了一下而已

transfor_2相当于从一个队列里面取得t，然后根据t来存钱，这个事务做完以后再把队列里面的t删掉，act2和3都是删除已经处理完了的t数据
在这里插入图片描述
保存一下后发现关于close这个地方竟然变红了，这是为什么呢？其实有这么一种情况，就是这个账户a当前余额为0，但是此时有账户向这个账户a转账，这个时候其实我们明显不应该执行关闭账户的操作，为了排除这种错误的行为，我们要在close中添加额外约束

按照刚才所述，我们不能在aq_of_trans的映射表里面找到该账户a，所以我们写下了下面的语句

$\notin dom(ran(aq\_of\_trans))$

其实不难理解，ran就是取值域，原本函数是t–><a,q>，取值域就是<a,q>，然后再来一个dom取定义域，对于<a,q>这个东西来说前面的a是定义域，后面的q是值域
在这里插入图片描述
OK，大功告成，证明义务也处理完毕，第一次精化结束

第二次精化

第二次精化用的是上课的代码，唯一的区别是t的映射不同，这里的写了俩映射t–>a和t–>q，而上面的是t–> <a,q>，问题不大，重点是添加了什么

第二次精化开始，在这里我们要完成FUN-5，想想看还是蛮简单的，只要给账户多一个类型的定义就OK了

让ct2继承ct1
在这里插入图片描述
定义两个常量normal和saving分别作为账户的类型，type作为存储类型的集合，这里要注意一下normal和saving不能相等

写到这里肯定有个大大问题，类型一个两个还好说，要是来十个，写不等号就要写死人，用内置函数partition可以让axm里面的语句可以用一句 $partition(type, {normal},{saving})$ 来代替

同理，mac3精化mac2，这边再加一个类型函数account_type，代表含义为某个账户的类型是什么
在这里插入图片描述
账户类型肯定要在开户的时候定义，在open里面写上

close销户的时候同样也要把这个映射移除

最重要的事件来了，因为上一步骤中我们设计的转账功能可扩展性良好，所以这里扩展也是相当方便，定义一个新的事件，我叫它saving_money_withdraw，它精化transfor_1

解释一下，这个事件就是处理同一个用户从normal账户到saving账户的转账请求，做出的action是将normal的钱扣除，然后将转账的账户a和钱的数量写入t，这时候有人会问题了，那么存钱呢？存钱的事情压根不用管，因为只要写好记录t，自然有前面的transfor_2处理
在这里插入图片描述
要添加的条件就是用户的owner是同一个，并且约束账户类型，从normal转到saving

另外其他的地方我也做了小小的限定，就当给需求文档添加约束吧