mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
974ef24c68
This is a proof of concept of the external printing/parsing. This works by adding externally defined (from Pretty) elements to the standard printing/parsing. We use the example of the Python plugin to show how it works: - the tasks should contain new notations (example python: /\ replaced by "and") - the new notations can be used in the transformations (example python: "assert (0 == 0 and b > 1)" The file format contained in the session is used to decide which external parser/printer to use. These are registered in a similar way that language, parser, or transformations are registered. For example, a goal whose ancestor is a python file (according to the file format inside the session) will be printed with the Python external printer; and transformations originating from this goal will be parsed with the same language.
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