How to validate method outcome.
Question: How can I write DbC that validates a method outcome based on method parameters. For example:
For a method named 'add':
if (a == 10) and (b == 20) the return value must be 30 otherwise it's a postcondition violation.
Comments
/**
* @post (i1==10)&&(i2==20) ? $result==30 : true
*/