diff --git a/src/bin_runtime b/src/bin_runtime
index eac7cab..e2ecc4c 100644
--- a/src/bin_runtime
+++ b/src/bin_runtime
@@ -1,4 +1,4 @@
 
 ======= token.sol:Token =======
 Binary of the runtime part: 
-608060405234801561001057600080fd5b50600436106100625760003560e01c8063095ea7b31461006757806318160ddd146100cd57806323b872dd146100eb57806370a0823114610171578063a9059cbb146101c9578063dd62ed3e1461022f575b600080fd5b6100b36004803603604081101561007d57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803590602001909291905050506102a7565b604051808215151515815260200191505060405180910390f35b6100d5610334565b6040518082815260200191505060405180910390f35b6101576004803603606081101561010157600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff1690602001909291908035906020019092919050505061033a565b604051808215151515815260200191505060405180910390f35b6101b36004803603602081101561018757600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610605565b6040518082815260200191505060405180910390f35b610215600480360360408110156101df57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291908035906020019092919050505061061d565b604051808215151515815260200191505060405180910390f35b6102916004803603604081101561024557600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610781565b6040518082815260200191505060405180910390f35b600081600260003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506001905092915050565b60015481565b60007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054146104e657610465600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836107a6565b600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505b61052e6000808673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836107a6565b6000808673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506105b86000808573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836107b3565b6000808573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550600190509392505050565b60006020528060005260406000206000915090505481565b6000816000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054101561066a57600080fd5b816000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054036000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506107356000808573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836107b3565b6000808573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506001905092915050565b6002602052816000526040600020602052806000526040600020600091509150505481565b6000818303905092915050565b60008183019050828110156107c757600080fd5b9291505056fea265627a7a72305820830fcb7059ea072cf2b43c8b28e2ba82a9fbe8b940d64eab3cbf58e057775fa464736f6c634300050a0032
+608060405234801561001057600080fd5b50600436106100625760003560e01c8063095ea7b31461006757806318160ddd146100cd57806323b872dd146100eb57806370a0823114610171578063a9059cbb146101c9578063dd62ed3e1461022f575b600080fd5b6100b36004803603604081101561007d57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803590602001909291905050506102a7565b604051808215151515815260200191505060405180910390f35b6100d5610334565b6040518082815260200191505060405180910390f35b6101576004803603606081101561010157600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff1690602001909291908035906020019092919050505061033a565b604051808215151515815260200191505060405180910390f35b6101b36004803603602081101561018757600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610605565b6040518082815260200191505060405180910390f35b610215600480360360408110156101df57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291908035906020019092919050505061061d565b604051808215151515815260200191505060405180910390f35b6102916004803603604081101561024557600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505061073d565b6040518082815260200191505060405180910390f35b600081600260003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506001905092915050565b60015481565b60007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054146104e657610465600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205483610762565b600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505b61052e6000808673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205483610762565b6000808673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506105b86000808573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020548361077c565b6000808573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550600190509392505050565b60006020528060005260406000206000915090505481565b60006106676000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205483610762565b6000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506106f16000808573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020548361077c565b6000808573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506001905092915050565b6002602052816000526040600020602052806000526040600020600091509150505481565b600081830390508282111561077657600080fd5b92915050565b600081830190508281101561079057600080fd5b9291505056fea265627a7a72305820fc55c2299637172ba4dc888e4933ab5e3235806bfa750a8469428c8c54b867f564736f6c634300050a0032
diff --git a/src/spec.md b/src/spec.md
index 35c9e5d..991da05 100644
--- a/src/spec.md
+++ b/src/spec.md
@@ -11,7 +11,7 @@
 
 <!-- END doctoc generated TOC please keep comment here to allow auto update -->
 
-# Balance
+### Balance
 ```act
 behaviour balanceOf of Token
 interface balanceOf(address Who)
@@ -30,7 +30,7 @@ iff
 
 returns Balance
 ```
-# Total Supply
+### Total Supply
 
 ```act
 behaviour totalSupply of Token
@@ -51,7 +51,7 @@ iff
 returns Supply
 ```
 
-# Allowance
+### Allowance
 
 ```act
 behaviour allowance of Token
@@ -72,7 +72,7 @@ iff
 returns Allowance
 ```
 
-# Transfer
+### Transfer
 ```act
 behaviour transfer-diff of Token
 interface transfer(address To, uint Value)
@@ -128,7 +128,7 @@ if
 
 returns 1
 ```
-# TransferFrom
+### TransferFrom
 
 ```act
 behaviour transferFrom-diff of Token
@@ -193,7 +193,7 @@ if
 returns 1
 ```
 
-# Approve
+### Approve
 
 ```act
 behaviour approve of Token
diff --git a/token.sol b/token.sol
index 70bf1d5..36bebdc 100644
--- a/token.sol
+++ b/token.sol
@@ -21,33 +21,37 @@ contract Token {
   uint public totalSupply;
   mapping (address => mapping (address => uint256)) public allowance;
 
+  constructor(uint supply) public {
+    totalSupply = supply;
+    balanceOf[msg.sender] = supply;
+  }
+
   function add(uint256 x, uint256 y) internal pure returns (uint z) {
     z = x + y;
     require(z >= x);
   }
   function sub(uint256 x, uint256 y) internal pure returns (uint z) {
     z = x - y;
+    require(z <= x);
   }
-  constructor(uint supply) public {
-    totalSupply = supply;
-    balanceOf[msg.sender] = supply;
-  }
-  function transfer(address receiver, uint256 value) public returns (bool) {
-    require (balanceOf[msg.sender]>= value);
-    balanceOf[msg.sender] = balanceOf[msg.sender] - value;
-    balanceOf[receiver]   = add(balanceOf[receiver], value);
-    return true;
-  }
-  function approve(address guy, uint wad) public returns (bool) {
-    allowance[msg.sender][guy] = wad;    
+
+  function transfer(address dst, uint256 value) public returns (bool) {
+    balanceOf[msg.sender] = sub(balanceOf[msg.sender], value);
+    balanceOf[dst]        = add(balanceOf[dst], value);
     return true;
   }
-  function transferFrom(address src, address dst, uint wad) public returns (bool) {
+
+  function transferFrom(address src, address dst, uint value) public returns (bool) {
     if (!(allowance[src][msg.sender] == uint(-1))) {
-      allowance[src][msg.sender] = sub(allowance[src][msg.sender], wad);
+      allowance[src][msg.sender] = sub(allowance[src][msg.sender], value);
     }
-    balanceOf[src] = sub(balanceOf[src], wad);
-    balanceOf[dst] = add(balanceOf[dst], wad);
+    balanceOf[src] = sub(balanceOf[src], value);
+    balanceOf[dst] = add(balanceOf[dst], value);
+    return true;
+  }
+
+  function approve(address guy, uint value) public returns (bool) {
+    allowance[msg.sender][guy] = value;
     return true;
   }
 }