pragma solidity 0.5.11;

contract FooToken {
  uint256 private _totalSupply;
  mapping (address => uint256) public _balances;
  mapping (address => mapping (address => uint256)) private _allowances;

  event AssertionFailed(string message);

  modifier transferEnsures(address _to) {
    uint256 oldSum = balanceOf(msg.sender) + balanceOf(_to);

    _;

    if (oldSum != balanceOf(msg.sender) + balanceOf(_to)) {
      emit AssertionFailed("postcondition of transfer failed");
    }

    assert(oldSum == balanceOf(msg.sender) + balanceOf(_to));
  }

  constructor() public {
    _totalSupply = 1000000;
    _balances[msg.sender] = 1000000;
  }

  function totalSupply() external view returns (uint256) {
    return _totalSupply;
  }

  function balanceOf(address _owner) public view returns (uint256) {
    return _balances[_owner];
  }

  function allowance(address _owner, address _spender) external view returns (uint256) {
    return _allowances[_owner][_spender];
  }

  function transfer(address _to, uint256 _value) transferEnsures(_to) public returns (bool) {
    address from = msg.sender;
    require(_value <= _balances[from]);
    uint256 newBalanceFrom = _balances[from] - _value;
    uint256 newBalanceTo = _balances[_to] + _value;
    _balances[from] = newBalanceFrom;
    _balances[_to] = newBalanceTo;
    emit Transfer(msg.sender, _to, _value);
    return true;
  }

  function approve(address _spender, uint256 _value) external returns (bool) {
    address owner = msg.sender;
    _allowances[owner][_spender] = _value;
    emit Approval(owner, _spender, _value);
    return true;
  }

  function transferFrom(address _from, address _to, uint256 _value) external returns (bool) {
    uint256 allowed = _allowances[_from][msg.sender];
    require(_value <= allowed);
    require(_value <= _balances[_from]);
    _balances[_from] -= _value;
    _balances[_to] += _value;
    _allowances[_from][msg.sender] -= _value;
    emit Transfer(_from, _to, _value);
    return true;
  }

  event Transfer(address indexed _from, address indexed _to, uint256 _value);
  event Approval(address indexed _owner, address indexed _spender, uint256 _value);
}