mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
2cc29e8963
- added break and continue - added range with one, two or three argument(s) - added slice (`list[i1:i2]`) - added negative index (`list[n], with -len(list) ≤ n < len(list)`) - added lists methods: - `list.append(n)` - `list.pop()` - `list.clear()` - `list.sort()` - `list.reverse()` - added `is_permutation(list1, list2)` predicate - added assignment operators `+=`, `-=`, `*=`, `//=`, `%=` - functions can now return `bool` and `list`
A plugin to verify programs written in a (microscopic) fragment of Python. Designed for teaching purposes. See tests/python/*.py for examples. Limitations wrt Python: - types are limited to integers and lists of integers - a list is not resizable (i.e. it is a mere array) - a function must return an integer or nothing Todo: - function/predicate with a definition (currently not supported); note: we would need to provide the type (int/array) of the arguments