system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
#### approve

- Allows `s` to access up to `v` tokens from your account as needed.
- If called again, it replaces the previous approval with the new `v`.


``` js
function approve(address s, uint256 v) public returns (bool success)
```
assistant
/// @notice postcondition (_allowed[msg.sender][_spender] == _value && success) || (_allowed[msg.sender][_spender] == __verifier_old_uint(_allowed[msg.sender][_spender]) && !success)
function approve(address _spender, uint256 _value) public returns (bool success);