• 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.
    15fc3d65
Name
Last commit
Last update
..
coq-tactic Loading commit data...
core Loading commit data...
driver Loading commit data...
ide Loading commit data...
jessie Loading commit data...
mlw Loading commit data...
parser Loading commit data...
printer Loading commit data...
server Loading commit data...
session Loading commit data...
tools Loading commit data...
transform Loading commit data...
trywhy3 Loading commit data...
util Loading commit data...
why3doc Loading commit data...
why3session Loading commit data...
whyml Loading commit data...
config.sh.in Loading commit data...