·
169 commits
to develop
since this release
In addition to several improvements and bug fixes, this release includes the following new functionalities:
- Support for refinement types
- A new built-in operator, any, to denote an arbitrary stream of values
- Realizability checks for contracts of non-imported nodes and refinement types
- It also checks the realizability of a node's environment. The check can be disabled by passing
--check_environment false
- It also checks the realizability of a node's environment. The check can be disabled by passing
- A new type constructor, history, to refer to an unbounded number of previous values of a stream
- Automatic generation of assumptions to ensure the satisfaction of a node's properties
Please refer to the CHANGES file for a more detailed description and to the user documentation for more details.