Articles

Whiley v0.3.31 Released!

The latest release is upon us, after a short break whilst I was holidaying in Europe!  This includes a few simple bug fixes and updates (see #433 and #392), along with one significant feature:

  1. Improved Context Information for Verification Errors (#435).  When a verification error occurred, it was often difficult to tell which part of a pre-condition / post-condition was causing it.  Now, context information is included to identify the relevant part of the precondition or postcondition.

As an example to illustrate this context information, consider the following (incorrect) program:

function abs(int x) => (int r)
ensures r == x || r == -x
ensures r >= 0:
    //
    return x

Compiling this program using the previous version of the compiler (with verification enabled), produced the following error:

./test.whiley:5: postcondition not satisfied
    return x
    ^^^^^^^^

However, this does not tell us which component of the postcondition actually failed. Compiling with the new version gives the following error:

./test.whiley:5: postcondition not satisfied
    return x
    ^^^^^^^^

./test.whiley:3: 
ensures r >= 0:
        ^^^^^^

Here, we see that the context information consists of additional point(s) in the program which are related. In this case, it tells us exactly which component of the postcondition is not satisfied.

As usual, you can get the latest files here:

wdk-src-v0.3.31
Created on October 8, 2014. 313 Downloads, 4.0 MB.
BSD License
wyjc-all-v0.3.31
Created on October 8, 2014. 441 Downloads, 2.5 MB.
BSD License

Leave a Reply

 

 

 

You can use these HTML tags

<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>