Skip to content
Snippets Groups Projects
  • Etienne Kneuss's avatar
    9c7e02b5
    Introduce support for methods and multiple objects/fields · 9c7e02b5
    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.
    9c7e02b5
    History
    Introduce support for methods and multiple objects/fields
    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.