Articles

Whiley v0.3.37 Released!

Another big update to Whiley landed today, and includes a whole raft of changes. In particular, various algorithms in the automated theorem prover have been reworked to improve performance (though more still needs to be done here). A rough summary of the changes in this version is:

  • Performance Improvements for Automated Theorem Prover.  In particular, the automated theorem prover is updated to the latest version of WyRL (v0.4.3).  The main improvements are: 1)  the rewrite history is now managed through a single Automaton (#17,#18); 2) an incremental algorithm for implementing efficient rewrite() is included, though it is not yet properly incremental (#19,#28).
  • Updates to Theorem Prover Rewrite Rules.  In particular, for the new requires clause which is now supported by WyRL (#548).
  • Improved to Standard Library Specifications.  Various methods in the standard library (replace(), slice(), append(),indexOf(),lastIndexOf()) have had their specifications updated to be more complete.  The work to fully specify all parts of the standard library is ongoing, however (#530).
  • Various misc. bug fixes (#536,#539,#541,#550).

At this point, the next major improvements I plan to work on are to get type invariants working properly again (#538,#528,#469,#468), and to continue refactoring the compiler ( e.g. #502,#501,#474).  That should keep me busy enough for a while!  As usual, you can get the latest version here:

wdk-src-v0.3.37
Created on December 16, 2015. 164 Downloads, 2.9 MB.
BSD License
wyjc-all-v0.3.37
Created on December 16, 2015. 397 Downloads, 2.4 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>