-
Etienne Kneuss authored
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.
Etienne Kneuss authoredMethods: -------- 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.