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 efficientrewrite()is included, though it is not yet properly incremental (#19,#28). - Updates to Theorem Prover Rewrite Rules. In particular, for the new
requiresclause 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:
