Postconditions that depend on method arguments?

LegacyForum

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.

LegacyForum

Put in the javadoc for the method the following line:

CODE

/**
* @post (i1==10)&&(i2==20) ? $result==30 : true
*/