• Andrei Paskevich's avatar
    WhyML: check type invariants · 15fc3d65
    Andrei Paskevich authored
    Type declarations for records (incuding the private records) can
    now be followed by a "witness": a set of values for the record
    fields that must satisfy the type invariant (if any). The fields
    must be initialized with pure terminating program expressions.
    The current syntax, proposed by Martin, is
        type t 'a = { f: ty1; g: ty2 }
          invariant { J[f,g] }
          by { f = e1; g = e2 }
    The generated proof obligation is the VC for
        let g = e2 in let f = e1 in assert { J[f,g] }
    In absence of an explicit witness, an existential proof obligation
    "exists f,g. J[f,g]" is produced.
pmodule.ml 46.2 KB