|Tags||jvm whiley java programming-language static-typing|
0.6.004 Sep 2018 06:45 minor feature: Add precondition to infinite loop when on function f. . Add invariant to sorted property. . Add specification for empty arrays in property sorted. . . . . . . . Add test case for #861. . Updated to WyCC feature/7-build. . Merge branch 'feature/7-build' into develop. . Merge branch 'develop'.
0.5.914 Jun 2018 03:17 minor feature: Remove Type.Intersection and Type.Difference . SemanticType FowardPropagation. . Moved more stuff into FlowTypeUtils. . Working on handling lifetime arguments. . Restored operand checking for equality operators. . Ripping out forward propagation. . Design for ReadWriteTypeExtractor. . Merge branch 'feature/844-syntype' into develop. . Add AbstractTypedVisitor and AmbiguousCoercionCheck. . Partial for ConcreteTypeExtractor. . Working on Type.Recursive. . Add Ref implementation. . for TypeSubtractor and Invalid Tests. . Updated dependency. . Merge branch 'feature/837-ambiguous' into develop. . Continuing work on ambiguous coercions. . Support coinduction to remove infinite loops. . Add support for expansion. . for AmbiguousCoercionCheck. . for type subtraction. . Merge branch 'feature/837-ambiguous' into develop. . Update test cases #854. . Support Binary and Hex Literals. . Merge branch 'feature/854-binlits' into develop. . Refactor to use BinaryRelation. . Add RecursiveTypeAnalysis. . Add WyllFile and accompanying compile task. . Add Wyll Interpreter. . Terminating this branch. . Merge branch 'feature/803-wyll' into develop. . Preparing next release. . Merge branch 'develop'.
0.5.802 Apr 2018 10:25 minor feature: Update to counterexample failure handling . Updating to latest WyTP. . Merge branch 'develop'.
0.5.729 Mar 2018 10:25 minor feature: Temporary remove intersection types #843 . Update to latest WyTP version. . Merge branch 'develop'.
0.5.621 Dec 2017 11:05 minor feature: for failing test case . Remove type 'any'. . Remove negation types from source syntax #827. . invalid test cases #827. . Marked test case #829. . Merge branch 'feature/827-any' into develop. . Add new test case. . Replace Type.Negation with Type.Difference #827. . for isVoid(Conjunct,LifetimeRelation). . for StrictSubtypeOperator.isVoid(). . AbstractTypeExtractor.toDisjunctiveNormalForm(Type.Difference). . for ReadableTypeExtractor.subtract(Type.Record). . Updated invalid test case outputs #827. . Merge branch 'feature/827-anyneg' into develop. . for subtype unit tests #827. . Uncommented previously commented tests. . Add recursive test case. . for Decl.Lambda type information #834. . Add recursive property test case. . Add Decl.Lambda.getCapturedVariables() #836. . Correction for broken test. . Merge branch 'develop'.
0.5.527 Oct 2017 06:25 minor feature: for Pretty Printing. Implement DefiniteUnassignmentCheck. Initial implementation of final modifiers #823. Complete implementation of final modifier #823. Merge branch 'feature/823-final-modifier' into develop. for verification of switch #823. Merge branch '/825-switch' into develop. Preparing next release. Merge branch 'develop'.
0.5.414 Oct 2017 14:05 minor feature: Add various test cases. for #820. Merge branch '/820-visitor' into develop. Adding more loop tests cases!!. Add BubbleSort test cases. Add test case based around cards. for #714. Proper for #714. Merge branch '/714-funpre' into develop. Preparing next release version. Merge branch 'develop'.
0.5.210 Oct 2017 03:16 minor feature: Add interesting verification test. Add test cases. Uncommented passing tests. Preparing next release version. Merge branch 'develop'.
0.5.105 Oct 2017 06:45 minor feature: for typing indirect invocations. Tweaked Visitors. MoveAnalysis #797. Merge branch 'feature/797-move' into develop. for parsing numbers and identifiers #603. Merge branch '/603-parsing' into develop. Add support for record and array borrows #798. Merge branch 'feature/798-move' into develop. for Record/Array Borrows. Add test case for #801. Use visitor to traverse expressions / preconditions. for #800. Merge branch '/assert' into develop. ReadableExtractors - ReadableTypeExtractor. Writeable*Extractor - WriteableTypeExtractor. Add TypeSystem.extractReadableType(). Merge branch 'feature/802-typesimp' into develop. Support for typing empty array initialiser #692. Merge branch 'feature/692-emptyarray' into develop. Add VariableAccess.isMove(). Preparing next release version. Merge branch 'develop'.
0.5.025 Sep 2017 07:25 minor feature: Begin process of relicensing WhileyCompiler. Updated invalid test cases. Significant updates to compiler!!. Parser now operational. Updating Interpreter. Update FlowTypeChecker. Working on making tests pass. Various refactorings to improve structure. Add concept of "descriptors". Various additional. for record subtyping #762. for function/method subtyping. Ignored failing tests for 763 and 764. Updated VerificationConditionGenerator. Merge branch 'refactoring/747-types' into develop. Refactored WhileyFile Opcodes / Expressions #768. Merge branch 'feature/768-wyfile' into develop. Add types to all expressions #766. Add SingleParameterVisitor. Refactored Expr.RecordInitialiser to NaryOperator. Refactor Integer Expressions. Refactor SyntacticItem.getOperands(). Merge branch 'feature/766-types' into develop. Refactored DefiniteAssignmentAnalysis. Optimised DefiniteAssignmentAnalysis. Update MoveAnalysis to use Visitor. Update FunctionCheck following RFC/purity. for LogicalImplication. FlowTypeCheck now infers types. Merge branch 'feature/766-flowtype' into develop. for #777. Merge branch '/777-from' into develop. for resolving external names. Merge branch '/776-resolution' into develop. for pre/postcondition macros. Deging missing span information. for associating spans with SyntacticItems. for translating binary operators. for Value.UTF8 constants. for spans and verification conditions. Various for translating constants unknowns. for loop invariants. for loop invariants #780. Numerous for VerificationConditionGenerator #780. Tidied up invalid test cases. Merge branch '/780-vcg' into develop. Further updates to VerificationConditionGenerator #780. empty type check #783. Merge branch '/783-void' into develop. for StaticVarLVals and Negations. for checking incomparable operands. for duplicate case conditions #648. for return statement checking. for comparable operands for runtime type test. for subtyping over references. Reworked Strict/Coercive SubtypeOperators. Tidied
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.1431 Jul 2017 01:05 minor feature: Trying to Travis. for name resolution. Update Ant Task for Extensibility. 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.3521 Jun 2015 07:25 minor feature: Source code (zip) . Source code (tar.gz).
0.3.3405 Jun 2015 20:25 minor feature: Source code (zip) . Source code (tar.gz).
0.3.3324 May 2015 13:45 minor feature: For ChangeLog see https://github.com/Whiley/WhileyCompiler/issues?q=milestone 3Av0.3.33
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.
ManageYou can also help out here by:
← Update project
or flagging this entry for moderator attention.
Share project 92