transfer.act

behaviour init of Token
interface constructor(string _symbol, string _name, string _version, uint _totalSupply)

creates Token
    string name         := _name
    string symbol       := _symbol
    uint256 totalSupply := _totalSupply

    mapping(address => uint) balanceOf :=  [CALLER := _totalSupply]
    mapping(address=>mapping(address=>uint)) allowance := []


behaviour transfer of Token
interface transfer(uint256 value, address to)

iff

   CALLVALUE == 0
   value <= balanceOf[CALLER]
   CALLER =/= to => balanceOf[to] + value < 2^256

case CALLER =/= to:

   storage

     balanceOf[CALLER] => balanceOf[CALLER] - value
     balanceOf[to]     => balanceOf[to] + value

   returns 1

case CALLER == to:

   returns 1

behaviour transferFrom of Token
interface transferFrom(address src, address dst, uint amount)

iff

   value <= balanceOf[CALLER]
   src    =/= dst => balanceOf[dst] + value < 2^256
   CALLER =/= src => 0 <= allowance[src][CALLER] - value
   CALLVALUE == 0

case src =/= dst:

   case CALLER == src:

      storage

         balances[src] => balances[src] - value
         balances[dst] => balances[dst] + value

      returns 1

   case CALLER =/= src and allowance[src][CALLER] == 2^256 - 1:

      storage

         balances[src] => balances[src] - value
         balances[dst] => balances[dst] + value

      returns 1

   case _:

      storage

         allowance[src][CALLER] => allowance[src][CALLER] - value
         balances[src]          => balances[src] - value
         balances[dst]          => balances[dst] + value

      returns 1

case src == dst:

   returns 1