Articles

Whiley v0.3.27 Released!

The next release of Whiley is upon us.  This includes a large number of bug fixes, and a significant rewrite of the verifier.  Unfortunately, the verifier is not yet verifying many more examples, but it’s now placed to do so.  Specifically, the main highlights are:

  1. Better Support for Contractive Types.  Contractive types are those which cannot accept any value constructable within the language itself.  In essence, they are equivalent to void.  An example would be something like type Rec is { Rec x }.  This type is contractive because is only describes values of infinite height.
  2. Reworked Automaton Rewriter.  The IterativeRewriter is responsible for rewriting automatons, which goes to the heart of how the verifier works.  This component has been significantly reworked to eliminate numerous bugs.  Unfortunately, this has meant that performance is somewhat worse, and this will need to be addressed in the future.
  3. Quantifier Instantiation.  The verifier is now capable of performing much more advanced forms of quantifier instantiation.  More needs to be done here, however, but the basic framework is now in place.  See #399 and #379.

As usual, you can get the latest versions of the compiler from here:

wyjc-all-v0.3.27
Created on August 14, 2014. 430 Downloads, 2.5 MB.
BSD License
wdk-src-v0.3.27
Created on August 14, 2014. 310 Downloads, 4.0 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>