epfl-lara/leon — pull request #53 by colder (2014-02-17 17:14:12+00:00)
Title: Introduce support for methods and multiple objects/fields

Methods:
--------

Methods are now supported in ADT roots only (e.g. single case classes or
abstract classes). The phase `MethodLifting` converts them to normal
global functions which makes them transparent to the rest of Leon.

Introducing Leon Library:
-------------------------

Common structures and functionalities can be shipped as part of the
Library.scala file, which is a set of ADTs with methods.

Imported via `import leon.Library._`

New Annotations:
----------------

- @verified means library function will not be considered for verification
unless specifically given through --functions

- @proxy allows non-pure bodies, which will be silently ignored.
pre/post need to be in purescala.

Functions without bodies (e.g. proxy methods) are now materialized with
a choose construct automatically, replicating the post-condition. This
allows compilation to bytecode and execution of VCs refering to proxy
methods.

Tree Modifications:
-------------------
- FunDef now have params, not args.

- VarDecl is renamed ValDef.

- Added methods in ClassDef, as well as This and MethodInvocation,
both are converted to normal function calls by the MethodLifting
phase.