Whiley 0.4.9 💾

Whiley is a programming language with refinement types, extended static checking and an indentation-based syntax. It compiles to Java bytecode and runs per JAR-runtime on any JVM, which in turn allows to reuse existing Java libraries. The SDK includes a compiler (wyjc), documentation, a plugin framework, disassembler, and an Eclipse plugin.

minor feature: Updated front-end for Named Records #704. Updated FlowTypeChecker for Named Records. Merge branch 'feature/704-namedrec' into develop. ing build dependency. Begun updated VCG for WyTP v0.5.0. VerificationConditionGenerator now running again. Various so that VCG works better. Lots of. Updates to VerificationConditionGenerator. Updates for new WhileyTheoremProver. Update command structure. Generate correct verification errors. Support checking postconditions. for quantified expressions. for record assignment. Add support for properly checking post conditions. Updated to support FieldDeclaration. for expanding type invariants. for configuring target directories. for quantifiers. Support type test operators. for loop invariant macros. Updated verification tests. Preparing for feature completion. Merge branch 'refactor/710-wytp' into develop. Add support for checking type invariants #666. Support type invariant checking for invocations. Updated test cases which pass / fail. Classified all existing test cases. Merge branch 'feature/666-retinv' into develop. Updated test classifications. Update invalid test cases. Updated test cases now passing with latest WyTP. Add test cases for property syntax #711. Support for parsing / interpreting properties #711. Support VCG for properties. Final tidy up; properties now working!!. Merge branch 'feature/711-properties' into develop. for #667. Merge branch 'feature/667-modcheck' into develop. related to #711. Tidying up test cases for WyTP. Updated test cases. Update for changes to WyTP (Open Records). Updated test cases after WyTP for overloading. Added test case for intersections. Add Support for Field Aliases #718. Merge branch 'feature/718-alias' into develop. Updated to latest WhileyTheoremProver (0.5.4). for Nested Assignments + VCG #719. Merge branch '/719-recass' into develop. for #720. Merge branch '/720-loopinv' into develop. Preparing next release version. Merge branch 'develop'.

BSDL jvm whiley java programming-language static-typing