• 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
bench Loading commit data...
bin Loading commit data...
doc Loading commit data...
drivers Loading commit data...
examples Loading commit data...
lib Loading commit data...
misc Loading commit data...
modules Loading commit data...
opam Loading commit data...
plugins Loading commit data...
share Loading commit data...
src Loading commit data...
tests Loading commit data...
theories Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.mailmap Loading commit data...
.merlin.in Loading commit data...
AUTHORS Loading commit data...
CHANGES Loading commit data...
DEVELOPER.readme Loading commit data...
INSTALL Loading commit data...
LICENSE Loading commit data...
Makefile.in Loading commit data...
OCAML-LICENSE Loading commit data...
README Loading commit data...
ROADMAP Loading commit data...
TODO Loading commit data...
Version Loading commit data...
check.sh Loading commit data...
configure.in Loading commit data...