mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
16 lines
468 B
Plaintext
16 lines
468 B
Plaintext
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
|
|
|
|
|