Whiley 0.4.17

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.

Tags jvm whiley java programming-language static-typing
License BSDL
State prerelease

Recent Releases

0.4.1716 Aug 2017 14:25 minor feature: Removed examples. for simplification of property types. Update after refactoring WyCC / WyTP. Merge branch 'develop'.
0.4.1604 Aug 2017 06:05 minor feature: Ignoring test which is taking too long on Travis. Updating to latest version of WyCC. Tagging next release version. Merge branch 'develop'.
0.4.1317 Jul 2017 03:16 minor feature: Updated to latest WyTP. Add support for printing proofs. Added test ignores for WyTP#124. eliminate use of "this" identifier in WyAL. for local names in WyalFiles. Change JDK used by Travis. Add ability to generate counterexamples. Updated WyTP dependency. Preparing next release version. Merge branch 'develop'.
0.4.1204 Jun 2017 00:25 minor feature: Uncomment passing tests. Tidied up valid verification tests. for whileypath command-line option. Updated VCG to include better source file info. Merge branch 'feature/746-errvcg' into develop. Remove deging code. Update failing verification tests. Updated passing verification tests. Updating classification of test cases. Updating passing tests. Updated more test cases. Implemented #751. Merge branch 'feature/751-typeinv' into develop. Test Case #730. Specification of Test Case #730. Merge branch 'feature/730-tests' into develop. Reclassified two test cases. Unignore test cases now passing. Remove SyntacticType.NonUnion interface #752. Replace SyntacticType with WyalFile.Type #752. Merge branch 'refactor/752-syntype' into develop. Add --vcg command-line option. Merge branch 'feature/753-vcg' into develop. Preparing next release version. Merge branch 'develop'.
0.4.1119 May 2017 03:16 minor feature: Working through test cases. Correct invalid test case. Correct test cases. Finished verification test classification. Add Support for Verification with Multiple Returns. Merge branch 'feature/713-multiret' into develop. Updating to Latest WyTP API. Merge branch 'feature/wytp-namespace' into develop. Update to WyTP v0.5.7. Parser and VCGen for Deref expressions. for #744. Add support for translating deref operator #743. Merge branch 'feature/742-deref' into develop. for #745. Merge branch 'feature/745-lambda' into develop. Preparing next release version. Merge branch 'develop'.
0.4.1008 May 2017 17:05 minor feature: Updated Ant Task to report compiled verified. Updated passing test cases. for WyilFilePrinter; updated passing tests. for reading IndirectInvoke bytecodes. Two for MoveAnalysis. Another for MoveAnalysis. Minor to MoveAnalysis. Revert "for reading IndirectInvoke bytecodes". Preparing for Next Release. Merge branch 'develop'.
0.4.919 Apr 2017 12:05 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'.
0.4.824 Feb 2017 01:05 minor feature: Preliminary implementation of MoveAnalysis #706. Merge branch 'feature/706-borrow' into develop. Partial for problem with command-line arguments. for VerificationConditionGenerator. Preparing next release version. Merge branch 'develop'.
0.4.725 Nov 2016 08:25 minor feature: Removed several now unused classes #700. Removed Automata.canonicalise(). Removed unused TypeSystem Constants. Merge branch 'feature/700-wyautl' into develop. Added verify attribute support to Ant task. Added includes attribute to Ant task. Ant task so builds fail properly. Merge branch 'feature/701-ant' into develop. Testing change for Travis Build. Preparing next release version. Merge branch 'develop'.
0.4.610 Nov 2016 14:25 minor feature: Unable to deploy from Ant. Updated broken test cases. Corrected broken test case. Added additional contractive test case. Merge branch '/691-contractive' into develop. Minor to BinaryTypeWriter. Reverted pom.xml; updated build.xml. two broken test cases. Partial for #696. Merge branch '/696-subtypes' into develop. Updated project configuration; verbose flag. Merge branch 'develop'.
0.4.502 Nov 2016 10:45 minor feature: Reverted build system to use Ant. Merge branch 'feature/ant' into develop. Investigating build failures. Corrected problems with.classpath. Updated names for test cases. Updated build config. for pretty printing types. for #690. Merge branch 'feature/690-expand' into develop. Preparing next release version. Merge branch 'develop'.
0.4.428 Oct 2016 21:05 minor feature: Update Run command. Update LICENSE Header. Updates related to the Whiley2JavaCompiler. Merge branch 'develop'.
0.4.321 Oct 2016 08:25 minor feature: Add support for configuring bootpath. Merge branch 'feature/688-bootpath' into develop. Add verbose flag to AntTask. for Ant Task. Merge branch 'develop'.
0.4.118 Sep 2016 13:45 minor feature: Updated Eclipse configuration. Add new test case; bring type tests online. Develop new AntTask. Merge branch 'feature/ant' into develop. Merge branch 'develop'.
0.4.013 Sep 2016 17:05 minor feature: Removed theorem prover from repository #671. Merge branch 'feature/671-wytp' into develop. Added missing jar file. Remove concept of "Build Number". Removed module "wyjc" #673. Merge branch 'feature/673-wyjc' into develop. Extracted Whiley Standard Lib #674. Extracted Whiley Build System #675. Refactoring WhileyCompiler. Update package structure and tests/scripts. Inline wycs std library. Merge branch 'refactoring/476-plugins' into develop. Updated build settings for WyCC lib. Add Decompile Command-Line Option #676. Merge branch 'feature/676-decompile' into develop. Add concept of BuildConfiguration. Update to latest Feature implementation. Add module Activator + compile/decompile commands. Updated Compile Command. Implement Decompile / Run commands. testing process. invalid test cases. Merge branch 'refactoring/677-template' into develop. Removed Nominal.raw(). Remove Nominal. Update Representation of Types. Merge branch 'feature/629-nominal' into develop. Updating travis for Java 8. Update dependency for WyCC. Merge branch 'develop'.
0.4.0-prerelease10 Aug 2016 05:45 minor feature: for #465. Merge branch 'feature/465-intersection' into develop. Remove Bytecode.relabel() methods. Update Bytecode Representation to Structured Form. Updated existing code to use new bytecodes. Updating Interpreter to new Bytecode Form. Updated Interpreter.executeSingle(). Unignored test cases. Update BytecodeTranslators. Updated Wyil2JavaBuilder. Begun new VerificationConditionGenerator. Remove BytecodeForest and update compiler. for WyilFileWriter. Update Wyil2JavaBuilder. Complete reimplementation of VerificationConditionGenerator. Update Compiler to final SyntaxTree design. Minor tweaks to test cases. for precondition checks / havocing variables. Add implementation for AliasDeclarations. Added missing file. Added several invalid test cases. Tweaked documentation in CodeGenerator. Updated CodeGenerator to resolve Void problem. Updated Wyil2JavaBuilder for Flow Typing. Tidy up VerificationConditionGenerator. Tidied up WyC valid tests. Tidy up invalid tests. for #662. More tidying of valid/invalid test cases. Remove "no" quantifier #668. Final for #662. Tidy up verification tests. Implement Multiple Returns. Merge branch 'feature/620-bytecode' into develop. Minor tweaks to ensure it compiles on Travis CI. Add DefiniteAssignmentAnalysis #665. Merge branch 'feature/665-defassign' into develop. Refactored SyntaxError/InternalFailure #669. Merge branch 'feature/669-synerr' into develop. Tidied up code in examples/ directory. Minor tweak for WhileyLabs. Implemented Build.Graph #670. Merge branch 'feature/670-deps' into develop. Update and tidy build system. Merge branch 'develop'.
0.3.4028 May 2016 07:45 minor feature: parsing for address expressions. deterministic order in error message. . Add test cases for #608,#609,#610. Remove AttributedCodeBlock #474. Replace CodeBlock with CodeForest #474. WyIL: Update VcGenerator. WyJC: Update WyJC. Merge branch 'feature/474-blocks' into develop. spam stdout when running test cases on travis. . Remove Codes.Void and Codes.NULL_REG #502. Replaecd Unary/Binary/Not/Invert bytecodes. Removed LengthOf, IndexOf, ArrayGen bytecodes #502. Remove move bytecode #502. Refactored Interpreter #502. Refactor Jvm backend #502. Remove Codes.NewRecord #502. Remove Codes.Nop, Assign and NewObject #502. Refactor wyil.lang.Code #502. Refactor Expr.LengthOf into Expr.UnOp #502. Merged Codes into Bytecode #502. Removed method Interpreter.cleanse(). Refactor Bytecode.If #502. Remove Bytecode "Constructors" #502. Add explicit Not operator #502. WyIL: Encapsulate fields remove remap/registers. WyIL: Remove CodeUtils. WyIL: Encapsulate Constant fields. Merge branch 'feature/502-bytecodes' into develop. WyC: Refactoring CodeGenerator #621. WyC: Finished refactoring CodeGenerator #621. Merge branch 'feature/621-codegen' into develop. WyC: Removed syntax checks from CodeGenerator. Merge branch 'feature/625-checks' into develop. for #622 (broken test cases). Moved checks for break/continue to Parser #621. Merge branch 'feature/621-codegen' into develop. function subtyping. whiley.io.File. recognize function and method types as definite types (). refactor method type intersection. purity checker. for #639. Merge branch '/639-vroot' into develop. Prune some uninhabitable types. implement lifetimes. ignore failing test, see #641. Updated version and tested next release version. Merge branch 'develop'.
0.3.3912 Mar 2016 10:45 minor feature: contributor sign off. parameterized junit test case: scan the dir for all available files. making reference subtype invariant. adjust test cases and add one for #583. additional test cases. . Merge branch '/587-deref' into develop. sort test cases by name (). Rewrite diff logic for sysout in invalid test cases. Add support for Fail statement. precedence for type negation and reference operators. Allow filtering of tests run from command line. Simplify Token.Kind enum's display code. Update to slow-running test cases #601. Merge branch 'feature/601-tests' into develop. Update travis.yml. Updated version number ahead of release. for #597. Merge branch 'develop'.
0.3.3829 Jan 2016 08:25 minor feature: WyCS: Add check for unknown module #536. BUILD: Update standard library re: wycs files #536. Merge branch '/536-null' into develop. WyRT: Updated resize() specification #530. WyRT: Updated Array.indexOf() #530. WyRT: Updated Array.lastIndexOf() #530. Merge branch 'feature/530-arrays' into develop. WyC: Applied update for #539. Merge branch 'feature/539-where' into develop. WyC: for brief output #541. Merge branch '/541-brief' into develop. BUILD: for building wyjc-all. TESTING: Added another test case. WyJC: Update the build.xml to add WyCS stdlib. WyCS: Update to new WyRL Rewriter API #544. WyCS: Useful update to Solver #544. Merge branch 'feature/544-wyrl' into develop. BUILD: Updated dependencies and version number. WyCS: Update for hybrid Rewriter API. BUILD: Added latest WyRL jar. WyCS: Update rewrite rule annotations. Update to WyRL emacs mode. WyCS: Update solver to use requires #548. Merge branch 'feature/584-requires' into develop. WyRT: Update replace(), slice(), append() #530. Merge branch 'feature/530-arrays' into develop. WyCS: Update to verbose verification output. Update to latest version of WyRL. in Solver Arithmetic unit #550. Merge branch '/550-div' into develop. Ignored known failing tests. Update to WyRL v0.4.3. Merge branch 'develop'. Refactor List = Array #551. for #551. Create for Reference_Valid_6 #553. Merge branch '/551-deref' into develop. Add test case to illustrate #554. Add test case FunctionRef_Valid_11 #554. for #554. Renaming Nominal.List to Nominal.Array. Merge branch '/554-lambdas' into develop. Partial for #552. Add test case for runtime testing #552. Partial for type testing function refs #552. Add test case for #555. Merge branch '/552-wytype' into develop. Update CONTRIBUTING.md. Update README with build instructions. Update install instructions in README. Merge branch 'feature/558-README' into develop. Updated building from source instructions to have some more detail, a?. Update WyRL to v0.4.4. Remove Tuples #537. Update
0.3.3613 Sep 2015 06:45 minor feature: WyCS: Very minor. WyCS: Added another test case. WyIL: Possible for #500. Merge branch '/500-quants' into develop. WyC,WyIL: Updated syntax for quantifiers #505. TESTING: Updated test cases for #505. Merge branch 'feature/505-quants' into develop. WyCS: Added test case from initialise example. WyCS: Removing set types and operators. WyCS: Reworks quantifier instantiation. WyCS: for MacroExpansion #507. WyCS: Update test suite #507. WyCS: Removed ListAppend and ListSublist. WyCS: for #509. WyC: Removed SubList operator #471. WyC: Removed List ElementOf Operator #471. WyCS: Removed ListUpdate syntax #506. for #510. WyCS: Integrating new WyRL API. Merge branch 'feature/506-sets' into develop. Adds syntax for list generators to WyC #512. Merge branch 'feature/512-listgen' of github.com:Whiley/WhileyCompile?. BUILD: Update Eclipse classpath to use WyRL User Lib. Remove list append operator #513. Merge branch 'feature/513-append' of github.com:Whiley/WhileyCompiler?. WyCS: Possible big for #514. WyCS: for #514. Merge branch 'feature/514-listinit' of github.com:Whiley/WhileyCompil?. WyIL: Potential for #516. WyCS: Deging Boollist_valid_1. WyIL: Removed invalid error messages. WyCS: for array update #516. Merge branch 'feature/516-update' of github.com:Whiley/WhileyCompiler?. for verification of array generator #518. Merge branch 'feature/517-generator' of github.com:Whiley/WhileyCompi?. WyCS: for MacroExpansion #517. Merge branch 'feature/517-capture' of github.com:Whiley/WhileyCompile?. WyCS: Updates to test cases. WyCS: for #519. WyCS: Merge branch '/521' of github.com:Whiley/WhileyCompiler into develop. for #521. Merge branch '/521' of github.com:Whiley/WhileyCompiler into develop. WyC: Removed Empty Array Initialiser #520. TEST: Unignored a number of tests which now verify. WyCS: Removed boolean flag from ArrayT #520. WyCS: Tested updates to solver array type #520. TESTING: Reclassifying verification test cases. Merge branch 'feature/520-array' of github.com:Whiley/Whi
0.3.3130 Nov 2014 13:45 minor bugfix: Improved Context Information for Verification Errors: When a verification error occurred, it was often difficult to tell which part of a pre-condition / post-condition was causing it. Now, context information is included to identify the relevant part of the precondition or postcondition.