Tags

Version 0.7.1 (17-06-2020)

Features
--------

- Add `ListOps.noDuplicate`, and a contract for `Set#toList` (#746)
- Check match exhaustiveness in type checker (#737)

Improvements
------------

- Rearrange debugging options (#781)
- Change StdOut print functions to handle Any (#761)
- Improve error reporting (#756)
- Add `@inlineInvariant` flag to ADT invariant dispatch method (#744)
- Use static checks for `SetOps` methods (#742)
- Recommend using Z3 4.8.6 instead of 4.7.1 (#741)

Bug fixes
---------

- Fix `List#toScala` method (#778)

Version 0.7.0 (07-02-2020)

Features:

- Enable `--type-checker` by default (#721)
- Rework the termination checker to infer measures for recursive functions (#721)

Improvements:

- Relax mutual recursion check for functions/ADTs enough for TypeEncoding (#721)
- Add `List#toScala` and `List.fromScala` to the library (#708)
- Add methods `map`, `withFilter`, `toList`, and `toScala` to `Set` (#708)
- Add methods `keys`, `values`, `toList` and `toScala` to `Map` (#708)

Bug fixes:

- Add missing position in `FieldAccessors` phase (#734)
- Fix extraction of extern types with Dotty frontend (#708)

Version 0.6.2 (16-01-2020)

- Ensures invariants of ancestors cannot be weakened
- Limit parallelism when running stainless-actors tests
- Fix broken benchmark in TypeCheckerSuite
- Update Docker packaging script

Version 0.6.1 (13-11-2019)

Improvements
------------

- Modularize Dockerfile and automate Docker image release process
- Specify version of extra deps when extracting sources from JAR
- Change name of target directory for extracted sources

Bug fixes
---------

- Add missing @library annotation to stainless-algebra. Bump to 0.1.1
- Fix missing import in stainless-algebra. Bump to 0.1.2

Version 0.6.0 (07-11-2019)

Features
--------

- Enable strict arithmetic by default (#608)
- Introduce `stainless.math.wrapping` method to opt-out of overflow checks (#608)
- Add `@wrapping` annotation for function definitions (#608)
- Add ability to resolve extra source dependencies via Coursier (#715)
- Erase values classes (#712)
- Expose @invariant flag to user-land (#712)
- Lift invariants of value classes to a refinement type (#712)
- Implement Map#-- for finite maps (#705)
- Add List.empty method

Improvements
------------

- Enforce overriding of abstract vals with constructor params (#712)
- Ensure soundness of invariants in TreeSanitizer (#712)
- Lift refinements in lets into assertions (#712)
- Update ScalaZ3 to its latest release (bundling Z3 4.7.1) (#707)
- Disallow defining classes within a class body (#697)
- Document type aliases and type members (#686)
- Ensure type parameters with non-trivial bounds are properly encoded (#685)

Bug fixes
---------

- Fix null pointer exception when running --eval (#699)
- Fix warning about multiple library sources (#692)

Version 0.5.1 (12-09-2019)

Bug fixes:

- Fix bug in ScalaCompiler.topmostAncestors (#693)
- Fix warning about multiple library sources (#692)

Release version 0.5.0 (12-09-2019)

Features:

- Bump Scala version to 2.12.9 and update sbt to 1.3.0 (#629, #591)
- Add support for removing elements from Map (#688)
- Setting `stainlessEnabled := false` keeps both library sources and ghost elimination (#684)
- Include Stainless library sources even when verification is disabled in sbt plugin (#680)
- Add --config-file option to specify or disable configuration file (#648)

Improvements:

- Document type aliases and type members support (#686)
- Add Cont monad benchmark to model exceptions (#675)
- Make qed be of unit type with post-condition (#669)
- Do not consider built-in classes in override chain (#661)
- Induct flag only adds decreases check if type checker is enabled (#657)
- Improve position reporting for postconditions (#656)
- Remove warnings for asserts in extern functions (#651)
- Propagate @ghost annotation to variables introduced by calls to default copy getter (#643)

Bug fixes:

- Fix bad mutual recursion in GodelNumbering proof (#679)
- Ensure type parameters with non-trivial bounds are properly encoded (#685)
- Do not check model when invoking solver during partial evaluation (#676)

Version 0.4.0 (2019-08-23)

* Features:

- Support for type members in local classes  (#633)
- Report functions with missing positions in PositionChecker (#639)
- Add AmortizedQueue data structure to Stainless library (#635)
- Add debug section to show the full VC before simplification (#637)
- Add script to run tests on stainless-actors and bolts (#623)
- Ignore @library flag on typeclasses which have non-library subclasses (#595)
- Enable -feature and -unchecked scalac flags in embedded compiler (#610)
- Enforce sound equality tests (#605, #609)
- Port partial specification feature from Leon (#438)
- Add BoundedQuantifiers module to the library (#596)

* Improvements:

- Propagate @ghost annotation to variables introduced by calls to default copy getter (#643)
- Do not lift refinement into pre-/post-conditions when `--type-checker` is enabled (#620)
- Follow symbolic links when searching for base directory (#621)
- Check that methods are only overriden by methods with the same ghostiness (#615)
- Check that required tools are installed before packaging (#599)
- Add readability check for jars in script (#600)

* Bug fixes:

- Add missing serializer for LocalThis (#631)
- Fix malformed case object constructor method (#641)
- Use triple quotes and escape \u for extraClasspath and extraCompilerArguments (#626)
- Fix bug in AssertionInjector where unary minus was lost in strict arithmetic mode (#630)
- Fix DottyVerificationSuite not being run (non-initialized folder) (#627)
- Fix bug where anonymous inner classes would have same identifier (#619)
- Fix handling of super calls in case objects  (#618)
- Fix a bunch of issues with type members (#580)

Version 0.3.2 (16-06-2019)

- Improve support for type members and type aliases (#580)

Version 0.3.1 (09-06-2019)

- Add testcase for #532 (#589)
- Add documentation about the Gitter8 template, and re-order some sections (#588)
- Re-enable check for abstract methods overrides and consider methods of abstract classes with empty body to be abstract (#587)
- Dealias type aliases more eagerly (#585)
- Add microtests from recently closed issues (#578)

Version 0.3.0 (02-06-2019)

- Display counter-examples when using metals (#579)
- Add --no-colors option, for use via metals in VS Code
- Fix "a required artifact is not listed by module descriptor" error
- Microtests from recently closed issues (#578)
- Add FAQ extracted from the C4DT newsletter (#570)
- Use git-describe to compute version of artifact in packaging script
- Indexed recursive types and type-checking based VC generation (#479)
- Bump Inox version to 1.1.0-332-ga6cbf8e (#571)
- Fix report being shown twice (#567)
- Emit warning when dropping require/ensuring/assert in a user @extern function (#562)
- Update sbt docs and fix plugin publishing issues (#565)
- Make purity of requires and assertions depend on their bodies (#547)
- Fix effects checker for MutableMapUpdated tree (#563)

Version 0.2.2 (25-06-2019)

- Fix sbt plugin, metals integration, and tests (#556)
- Switch to git-describe based versioning scheme (#550)
- Add `--version` flag (#550)

Tag version 0.2.1

Release version v0.2.0-cfac3aaf