合约
**C := <a, bal, P, M>**
其中C代表一个合约，可以由一个元组组成，该元组如下：a表示合约的地址，bal表示合约中的余额，P表示该合约的用户，M和P是一一对应的关系，表示该用户在该合约中的账户余额，用M:P表示。
交易
t := < s, r, v>
其中，t表示一个交易，可以由一个元组组成，该元组如下：s表示发送者的地址，r表示接受者的地址，该交易表示从发送者s的余额中(s.bal)扣除v个ether给接收者r。
Pre(x)
交易发生前变量x的值。
Post(y)
交易发生后变量y的值。
余额不变性
对于每一个合约（此处关心的是外部账户和合约之间），**<a, bal, P, M>。**都存在一个等式，如下，
其中表示的意思是，对于该合约所有用户的总余额减去该合约的总余额是一个常数K。
交易不变性（没有考虑交易花费的Gas）
对于每一笔对外交易（此处关心的是两个合约之间），**<C.a, r, v>。**都存在一个等式，
其中，
r表示一个合约的地址，M(r)表示该地址在合约C中的账户余额。r.bal表示合约r的余额。等式的意思是账户r在合约C中的余额的变化量加上合约r的余额的变化量等于零。可以理解为两个银行之间转账，一个银行余额的减少量等于另一个银行余额的增加量。
