Mentions légales du service

Skip to content
  • Jean-Christophe Filliâtre's avatar
    new VC to prove well-foundedness of user-provided variants · 4af9081d
    Jean-Christophe Filliâtre authored
    fixes issue #57
    
    a new theory relations.WellFounded is introduced for this purpose
    (and must be imported whenever one wants to make use of a custom
    relation for a variant)
    
    it defines, inductively, a notion of accessibility for a given
    predicate R (x is accessible whenever all elements smaller than x for R
    are alreay accessible)
    
    whenever one has to prove that a variant decreases, a new VC is also
    generated, to show that the old value of the variant is accessible
    for the order relation
    
    note: accessibility being defined inductively, proving well-foundedness
    is out of reach of SMT solvers; but at least this is sound now
    4af9081d