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 efficientrewrite()
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).
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!