Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

  1. 11 Oct, 2019 1 commit
  2. 23 Aug, 2019 1 commit
  3. 25 Apr, 2019 1 commit
  4. 11 Feb, 2019 1 commit
  5. 26 Nov, 2018 1 commit
  6. 19 Oct, 2018 1 commit
  7. 18 Oct, 2018 1 commit
  8. 16 Oct, 2018 1 commit
  9. 14 Oct, 2018 1 commit
  10. 04 Oct, 2018 1 commit
  11. 28 Sep, 2018 2 commits
  12. 06 Aug, 2018 1 commit
  13. 17 Jul, 2018 1 commit
    • Andrei Paskevich's avatar
      Ident: disambiguated symbolic notation · 295cacf4
      Andrei Paskevich authored
      It is possible to append an arbitary number of quote symbols
      at the end of an prefix/infix/mixfix operator:
                  applied form      standalone form
                    -' 42               (-'_)
                    x +' y              (+')
                    a[0]' <- 1          ([]'<-)
      Pretty-printing will use the quote symbols for disambiguation.
      The derived symbols can be produced by Why3 by appending
      a suffix of the form "_toto" or "'toto". These symbols can
      be parsed/printed as "(+)_toto" or "(+)'toto", respectively.
  14. 07 Jul, 2018 1 commit
    • Andrei Paskevich's avatar
      confine all notation handling inside Ident · 0fea401c
      Andrei Paskevich authored
      This commit removes all hard-coded "infix ..", "prefix ..",
      and "mixfix .." from the rest of the code, and handles the
      symbolic notation entirely inside Ident. It does not change
      the notation itself.
  15. 17 Jun, 2018 1 commit
  16. 14 Jun, 2018 1 commit
  17. 05 Jun, 2018 1 commit
  18. 01 Jun, 2018 1 commit
  19. 17 May, 2018 1 commit
  20. 16 Apr, 2018 1 commit
  21. 21 Mar, 2018 1 commit
    • Guillaume Melquiond's avatar
      Homogenize constructor names. · 6ef0273e
      Guillaume Melquiond authored
      The pattern-matching construct in the logic is now systematically named
      "Tcase" in constructors (Ptree.Tmatch -> Tcase). The one in the
      programs (supporting exceptions) is now systematically named "Ematch"
      (Expr.Ecase -> Ematch, Dexpr.DEcase -> DEmatch). They are now homogeneous
      with the other constructors: Term.Tcase, Dterm.DTcase, Ptree.Ematch,
      Mltree.Ematch. Smart constructor Expr.e_case was renamed accordingly.
  22. 20 Mar, 2018 1 commit
  23. 11 Jan, 2018 1 commit
  24. 20 Nov, 2017 1 commit
  25. 19 Jul, 2017 1 commit
  26. 22 Jun, 2017 1 commit
    • 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.
  27. 11 Jun, 2017 1 commit
  28. 10 Jun, 2017 1 commit
    • Andrei Paskevich's avatar
      Mlw: slightly generalize the rules for overloading · 084211c1
      Andrei Paskevich authored
      A symbol is now considered overloadable if it satisfies
      the following conditions:
        - it has at least one parameter
        - it is non-ghost and has fully visible result
        - all of its parameters are non-ghost and have the same type
        - its result is either of the same type as its parameters
          or it is a monomorphic immutable type.
      An overloadable symbol can be combined with other symbols of the
      same arity and overloading kind. Otherwise, the new symbol shadows
      the previously defined ones.
      This generalisation allows us to overload symbols such as "size"
      or "length", and also symbols of arbitraty non-zero arity.
      I am reluctant to generalize this any further, because then we
      won't have reasonable destructible signatures for type inference.
  29. 08 Jun, 2017 1 commit
    • Andrei Paskevich's avatar
      Mlw: for-loops over range types · 2f7b69b5
      Andrei Paskevich authored
      In the surface language, the loop index is always int in
      the loop invariant and all annotations and pure terms inside
      the loop. If you want to access the original range-typed index,
      use "let copy_i = i in" in the program code before your assertion.
      Of course, you cannot do that for the loop invariant, which is
      what we want.
  30. 06 Jun, 2017 1 commit
  31. 05 Jun, 2017 1 commit
  32. 04 Jun, 2017 1 commit
    • Andrei Paskevich's avatar
      Mlw: overloaded symbols · 1aa6a8b1
      Andrei Paskevich authored
      This is a prototype version that requires no additional annotation.
      In addition to the existing rules of scoping:
        - it is forbidden to declare two symbols with the same name
          in the same scope ("everything can be unambiguously named"),
        - it is allowed to shadow an earlier declaration with a newer one,
          if they belong to different scopes (e.g., via import),
      we define one new rule:
        - when an rsymbol rs_new would normally shadow an rsymbol rs_old,
          but (1) both of them are either
            - binary relations: t -> t -> bool,
            - binary operators: t -> t -> t, or
            - unary operators:  t -> t
          and (2) their argument types are not the same,
          then rs_old remains visible in the current scope.
          Both symbols should take non-ghost arguments and
          return non-ghost results, but effects are allowed.
          The name itself is not taken into account, hence
          it is possible to overload "div", "mod", or "fact".
      Clause (1) allows us to perform type inference for a family of rsymbols,
      using an appropriate generalized signature.
      Clause (2) removes guaranteed ambiguities: we treat this case as
      the user's intention to redefine the symbol for a given type.
      Type inference failures are still possible: either due to
      polymorphism (['a -> 'a] combines with [int -> int] and
      will fail with the "ambiguous notation" error), or due
      to inability to infer the precise types of arguments.
      Explicit type annotations and/or use of qualified names
      for disambiguation should always allow to bypass the errors.
      Binary operations on Booleans are treated as relations, not as
      operators. Thus, (+) on bool will not combine with (+) on int.
      This overloading only concerns programs: in logic, the added rule
      does not apply, and the old symbols get shadowed by the new ones.
      In this setting, modules never export families of overloaded symbols:
      it is impossible to "use import" a single module, and have access to
      several rsymbols for (=) or (+).
      The new "overloading" rule prefers to silently discard the previous
      binding when it cannot be combined with the new one. This allows us
      to be mostly backward compatible with existing programs (except for
      the cases where type inference fails, as discussed above).
      This rule should be enough to have several equalities for different
      program types or overloaded arithmetic operations for bounded integers.
      These rsymbols should not be defined as let-functions: in fact, it is
      forbidden now to redefine equality in logic, and the bounded integers
      should be all coerced into mathematical integers anyway.
      I would like to be able to overload mixfix operators too, but
      there is no reasonable generalized signature for them: compare
      "([]) : map 'a 'b -> 'a -> 'b" with "([]) : array 'a -> int -> 'a"
      with "([]) : monomap -> key -> elt". If we restrict the overloading
      to symbols with specific names, we might go with "'a -> 'b -> 'c" for
      type inference (and even "'a -> 'b" for some prefix operators, such
      as "!" or "?"). To discuss.
  33. 03 Jun, 2017 2 commits
  34. 01 Jun, 2017 1 commit
  35. 22 May, 2017 1 commit
  36. 16 May, 2017 2 commits
  37. 12 May, 2017 1 commit