Postconditions that depend on method arguments?

LegacyForumLegacyForum Posts: 1,669 ✭✭
edited December 2016 in Jtest
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.
Tagged:

Comments

  • LegacyForumLegacyForum Posts: 1,669 ✭✭
    Put in the javadoc for the method the following line:

    CODE
    /**
    * @post (i1==10)&&(i2==20) ? $result==30 : true
    */
Sign In or Register to comment.