Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

  1. 08 Jun, 2018 1 commit
  2. 07 Jun, 2018 5 commits
  3. 06 Jun, 2018 5 commits
  4. 05 Jun, 2018 10 commits
  5. 04 Jun, 2018 5 commits
  6. 01 Jun, 2018 13 commits
  7. 31 May, 2018 1 commit
    • 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