Whiley 0.10.18
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.
Recent Releases
0.10.1802 Jan 2024 16:13
minor feature:
0.8.012 Oct 2020 02:45
minor feature:
Refactoring for WyCC
.
Update for latest WyCC / WyCLI.
.
Merge branch 'feature/61-cli' into develop.
.
Merge branch 'develop'.
0.7.307 Oct 2020 15:05
minor feature:
Update config.xml
.
.
.
.
Tweaks for QuickCheck.
.
Preparing next release version.
.
Merge branch 'develop'.
0.7.206 Sep 2020 17:05
minor feature:
Merge commit '8df2a1054' into develop
.
Preparing next release version.
.
Merge branch 'develop'.
0.7.107 Jul 2020 09:25
minor feature:
Detect Non-Export/Public Tests
.
for #1006.
.
Add interesting test case for objects.
.
.
Merge branch '/forloop-1010' into develop.
.
.
Remove lifetime syntax.
.
Compiler compiles again!.
.
tests for lifetimes.
.
Merge branch 'feature/1014-lifetimes' into develop.
.
Preparing next release version.
.
Merge branch 'develop'.
0.7.003 Apr 2020 06:45
minor feature:
Move list of ignored tests into TestUtils
.
Update syntax for destructuring assignment #979.
.
Update binary format.
.
.
Merge branch '/980-subtype' into develop.
.
More for tuples.
.
Add TupleInitialiser.toString().
.
Support for statements #982.
.
Merge branch 'feature/982-foreach' into develop.
.
Minor adjustements to FlowTypeCheck.
.
for #912.
.
Merge branch '/912-template' into develop.
.
for FlowTypeCheck.
.
Remove unknown reference #985.
.
Update for Reference Semantics #985.
.
Merge branch 'feature/RFC64' into develop.
.
Initial Design for New FlowTypeChecker.
.
Adds a bunch of test cases.
.
Backwards type inference works upto templates!.
.
Working on binding algorithm.
.
isSubtype now returns Constraints.
.
Implement constraints solving.
.
Merge branch 'feature/941-typeinf' into develop.
.
Updated Type Inference Algorithm.
.
Refactoring FlowTypeChecker.
.
Minor refactoring.
.
Merge branch 'feature/990-coercions' into develop.
.
Removed SubtypeOperator.LifetimeRelation #992.
.
Merge branch 'feature/992-lifetime' into develop.
.
Add test cases based on interview problem.
.
Beginning Strict Subtyping #998.
.
Add leastUpperBound/greatestLowerBound #998.
.
Support bounded existentials.
.
Working on forward type propagation.
.
Add Subtype Constraint Forms.
.
Change of tack.
.
Redesigned Push / Pull Mechanism.
.
Tidying up and documentation.
.
Merge branch 'feature/998-subtyping-s' into develop.
.
for valid verification tests.
.
Add test cases for #1004.
.
Preparing release version.
.
Merge branch 'develop'.
0.6.1302 Dec 2019 06:25
minor feature:
Restore build logging information
.
.
Merge branch '/969-check2' into develop.
.
TestUtils.
.
.
Merge branch '/972-templates' into develop.
.
.
Merge branch '/971-fn' into develop.
.
Add test case for #973.
.
for #974.
.
Merge branch '/974-arrinf' into develop.
.
Support Build.Meter.
.
Merge branch '/968-perf' into develop.
.
Improved build metering.
.
.
Add WyilFile.Type.Selector.
.
Implement Type.Selector generator.
.
Merge branch '/977-typerefine' into develop.
.
Remove Multiple Expressions #975.
.
Merge branch 'feature/975-tuples' into develop.
.
Support multiple variable declarations #979.
.
Merge branch 'feature/979-mvardecl' into develop.
.
Preparing next release.
.
Merge branch 'develop'.
0.6.1231 Oct 2019 06:25
minor feature:
Updating to latest version
.
.
Merge branch '/969-check' into develop.
.
Updates to QuickCheck.
.
for QuickCheck.
.
Support targetted checking #960.
.
Merge branch 'feature/960-qcnames' into develop.
.
QuickCheck sampling.
.
for WyilFilePrinter.
.
Merge branch '/55-prettyprint' into develop.
.
Another for WyilFilePrinter.
.
.
Update parser and WyilFile format.
.
Update NameResolution.
.
Support import from with multiple names.
.
Merge branch 'feature/967-importwith' into develop.
.
for import with.
.
for WyilFile initialisation.
.
Updated SyntacticItem Descriptors.
.
Create WyilFile.Attr section.
.
Working towards a true schema.
.
Finally implemented a Schema!!.
.
for new Schema.
.
WyilFile versioning is now operational #957.
.
Merge branch 'feature/957-wyilfile' into develop.
.
Prepating next release version.
.
Merge branch 'develop'.
0.6.1110 Oct 2019 10:25
minor feature:
from lgtm.org
.
Updated for latest WyCC API.
.
Remove deging code.
.
Preparing next release version.
.
Merge branch 'feature/17-wypm' into develop.
.
Merge branch 'develop' of github.com:Whiley/WhileyCompiler.
0.6.1013 Sep 2019 12:45
minor feature:
Minor update for Maven config
.
Add test cases from WyJS.
.
Add (and update) test cases.
.
for indirect invocations #946.
.
Merge branch '/946-indivk' into develop.
.
Initial mock-up of unknown reference types.
.
Add tests for unknown references.
.
Add explicit FieldDereference operator.
.
for subtype operator.
.
erge branch 'feature/rfc54-existentials' into develop.
.
.
Merge branch '/948-lambdas' into develop.
.
for type checking Decl.Lambda.
.
Add new test cases.
.
for #952.
.
Merge branch '/952-purity' into develop.
.
Add test case for WyJS.
Add and tests #951.
.
Merge branch '/951-npe' into develop.
.
for #950.
.
Merge branch '/950-flowtype' into develop.
.
for #882.
.
Updating to latest WyCC.
.
Merge branch 'develop'.
0.6.808 Aug 2019 06:05
minor feature:
Updating Travis config
.
for broken test case. #939.
.
for #939.
.
Merge branch 'feature/939-sigcheck' into develop.
.
for native methods #939.
.
Add missing output for invalid test.
.
Support Type.as() and Type.filter() #940.
.
Merge branch 'feature/940-underlying' into develop.
.
Add test case for #912.
.
Add test case for #912.
.
Merge branch 'feature/jmg4' into develop.
.
for JModelGen 0.4.0.
.
Remove Type.Any #942.
.
Merge branch 'feature/942-anytype' into develop.
.
Preparing next release.
.
Merge branch 'develop'.
0.6.702 Aug 2019 10:05
minor feature:
Add new test case
.
Add note about importing properties.
.
Support sanity checking import statements #933.
.
Merge branch 'feature/933-imports' into develop.
.
Prevent exposing private declarations #932.
.
and additions for test cases.
.
Merge branch 'feature/932-public' into develop.
.
Add test cases for #934.
.
Adding reference tests.
.
Add more test cases for templates.
.
Stripped out SemanticType #929.
.
Support record subtraction.
.
Update invalid tests to pass.
.
Merge branch 'feature/929-subtyping' into develop.
.
Preparing next release.
.
Merge branch 'develop'.
0.6.605 Jul 2019 03:25
minor feature:
for QuickCheck
.
for Interprete Returns.
.
for type invariants.
.
Merge branch '/921-vardecl' into develop.
.
Improved handling of internal failures.
.
for Exceptions Logging.
.
QuickCheck: remove QuickCheck.Generated LogEntry.
.
Support Interpreter Timeouts.
.
Merge branch 'feature/timeouts' into develop.
.
Add ignores configuration option.
.
Remove methods configuration flag.
.
Merge branch 'feature/ignores' into develop.
.
Update for Context.setIgnores().
.
Add support for static variable type invariants.
.
Merge branch '/923-static' into develop.
.
Add Copy Constructor for WyilFile.
.
QuickCheck: Add ability to record split time.
.
Add experimental feature for sampling.
.
QuickCheck: Improved sampling mechanisms.
.
Merge branch 'feature/sampling' into develop.
.
Update QuickCheck to use approximate sampling.
.
Working on extracting stack frame information.
.
Add support for StackTraces + Records.
.
Merge branch 'feature/frames' into develop.
.
Preliminary support for verification.
.
Significant updates for verification.
.
Updates for error messages.
.
Add failing test cases #925.
.
for type checking #925.
.
Merge branch '/925-typing' into develop.
.
Updates to handle parser errors.
.
for lexing #909.
.
Merge branch '/909-parsing' into develop.
.
Preparing next release version.
.
Merge branch 'develop'.
0.6.522 May 2019 07:05
minor feature:
Begun QuickCheck Command
.
QuickCheck: is generating primitive values.
.
Various to QuickCheck Interpreter.
.
Add rough ability for memoisation.
.
Merge branch 'feature/quickcheck' into develop.
.
Update QuickCheck for native methods.
.
Allow skipping methods in QuickCheck.
.
for type invariants.
.
for handling zero inputs.
.
Minor tweaks + identify irrelevant tests.
.
for undefinedness of input values #916.
.
for interpreter execution of properties #914.
.
for type generation and templates #913.
.
Merge branch 'feature/904-check' into develop.
.
Support logging intermediate type generation.
.
Update QuickCheck to support sampling.
.
Support command-line options in QuickCheck.
.
Tidying up QuickCheck.Context.
.
Improved output for QuickCheck.
.
Minor tweaks for testing quickcheck.
.
Add support to QuickCheck for sampling types.
.
Preparing next release version.
.
Merge branch 'develop'.
0.6.410 May 2019 06:05
minor feature:
TestUtils.findSyntaxErrors now public.
.
Remove InternalFailure.
.
Updating pom.xml.
.
Merge branch 'feature/896-synerr' into develop.
.
Removes throwSyntaxError.
.
Thought required!!!!.
.
Refactored for new build process.
.
Simplifying COmpileTask.
.
for command-line operation.
.
Tweaking logging process.
.
Put back logging code.
.
Remove redundant Build.Task.getIdentifier() concept.
.
Refactoring CompileTask.
.
Adapt CompileTask to latest Build.Task.
.
for verification.
.
Merge branch 'feature/45-build' into develop.
.
Support replace method.
.
Merge branch 'feature/51-replace' into develop.
.
Support garage collection.
.
Preparing next release version.
.
Updating to wycc-0.7.9.
.
Ignored tests.
.
Merge branch 'develop'.
0.6.320 Mar 2019 10:05
minor feature:
Remove SyntacticElement
.
Merge branch 'feature/10-synelement' into develop.
.
Update FlowTypeCheck for SyntacticItem.Marker.
.
Update Flow Type Checker.
.
Update DefiniteAssignment.
.
Improved error reporting.
.
Support for recovery.
.
Working on error reporting.
.
Lots of improvements to error recovery.
.
Commented out unresolvable tests.
.
Working on simpler mechanism for error recovery.
.
Implement stage termination.
.
for AmbiguousCoercionCheck.
.
Merge branch 'feature/884-synerr' into develop.
.
Reset SyntacticItem API.
.
Update WyCC dependency.
.
Support parsing template declaration #890.
.
Add support for template variables.
.
Merge branch 'feature/890-templates' into develop.
.
Update WyCC dependency.
.
for #891.
.
for #891.
.
for #894.
.
Preparing next release version.
.
Merge branch 'develop'.
0.6.211 Feb 2019 09:25
minor feature:
Update verification error messages.
.
Updating VerificationConditionGenerator.
.
Adding support for enabling verification.
.
Support verify build flag.
.
for VerificationConditionGenerator.
.
Update for logging support.
.
Add test cases for recursive properties.
.
Add recurive property example.
.
Add support for counterexample generation.
.
Implement counterexample attribute.
.
Merge branch 'feature/881-counterexample' into develop.
.
Minor for test cases.
.
Updates to invalid test cases.
.
Preparing next release version.
.
Merge branch 'develop'.
0.6.123 Jan 2019 03:16
minor feature:
Rework WhileyFileResolver #863
.
Merge branch 'feature/863-nameres' into develop.
.
Updating to latest release version.
.
Add new test case.
.
Refactor WhileyFile = WyilFile. Add WhileyFile #866.
.
Implement Platform.refresh(Graph).
.
Moving towards single monolithic WyilFile.
.
Updating mechanism for creating WyIL files.
.
Add support for naming WyIL file.
.
Updates for SyntacticHeap roots.
.
Add (incomplete) support for WyilFile.Decl.Module.
.
Update TestUtils.compile().
.
for error messages #866.
.
Strip out NameResolver #872.
.
Additional refactoring.
.
Working on NameResolution.
.
Continued working on NameResolution.
.
Various for NameResolution.
.
Function / Method overloading is working.
.
for interpreter.
.
for NameResolution.
.
Minor for QualifiedName.
.
for test case.
.
Remove NameID.
.
Working NameResolution External Import.
.
Resolving Externals in NameResolution.
.
Refactoring NameResolution.
.
Refactor NameResolution.
.
Updates to NameResolution.
.
Update NameResolution.
.
for importing stubbs #874.
.
Add squaring test case.
.
Improve syntax error reporting.
.
ADD PRINTABLE.
.
WyilFilePrinter.
.
Working on NameResolution.
.
Working on NameResolution.
.
Lots of changes to NameResolution.
.
Consolidationis now working.
.
in SymbolTable.consolidate().
.
Merge branch 'feature/866-wyil' into develop.
.
Update README.
.
for #876.
.
Merge branch '/876-unit' into develop.
.
for #875.
.
Merge branch '/875' into develop.
.
for #877.
.
Merge branch '=877-unresolved' into develop.
.
for #878.
.
for linking patches.
.
for interpreter invocation.
.
Various minor.
Merge branch 'develop'.
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.
|
Links Project Website Download→ GitHub Submitted by freshcodeManageYou can also help out here by:← Update project or flagging this entry for moderator attention. Share project
|