out (; balance == balance + amount) // checked after method returns
out (; balance == balance + amount) // checked after method returns
The correct way to go about this would be to return the new balance and capture the return value in the first part of the out postcondition like:
```D double deposit(double amount) in (amount > 0, "Deposit amount must be positive") out (result; result == balance) { balance += amount; return balance; } ```
My mistake!
double deposit(double amount)
in (amount > 0, "Deposit amount must be positive")
out (result; result == balance)
{
balance += amount;
return balance;
}