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

Grants `_spender` permission to withdraw tokens multiple times from your account up to the `_value` limit. If called again with a new value, it will update the current allowance.

**IMPORTANT**: To prevent known vulnerabilities, it's recommended to set the allowance to `0` before assigning a new `_value` for the same spender.


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