Welcome to the new Parasoft forums! We hope you will enjoy the site and try out some of the new features, like sharing an idea you may have for one of our products or following a category.

Postconditions that depend on method arguments?

LegacyForum
LegacyForum Posts: 1,664 ✭✭
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

  • LegacyForum
    LegacyForum Posts: 1,664 ✭✭
    Put in the javadoc for the method the following line:

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

Categories

Tagged