1. 14 Mar, 2014 1 commit
  2. 05 Mar, 2014 1 commit
  3. 17 Feb, 2014 1 commit
  4. 16 Feb, 2014 1 commit
  5. 14 Feb, 2014 3 commits
    • Andrei Paskevich's avatar
      WhyML: change the syntax of "abstract" · 4fd8b24d
      Andrei Paskevich authored
      The old syntax:   abstract expr [spec]...
      The semicolon binds more loosely than "abstract" and
      the specification clauses are optional, so that
      "abstract e1; e2" is the same as "(abstract e1); e2"
      and "abstract e1; e2; ensures {...}" is a syntax error.
      The new syntax:   abstract [spec]... expr end
      This allows to put sequences of expressions under "abstract"
      without ambiguity and moves the specification clauses to the
      beginning. In other words, "abstract" becomes a "begin" with
      a specification attached. The spec-at-the-top is consistent
      with the syntax of functions and the whole seems to be more
      natural for the intented use of "abstract" (a logical cut).
    • Andrei Paskevich's avatar
      WhyML: admit terminating semi-colons when there is no ambiguity · e66e2a3f
      Andrei Paskevich authored
        begin ... expr; end
        let fn x y = ... expr ; in ...
        match ... with pat -> ... expr ; | pat -> ... expr ; end
      In this way, it's much easier to add and remove additional
      assertions at the end of ()-typed blocks.
    • Andrei Paskevich's avatar
  6. 12 Feb, 2014 2 commits
  7. 20 Jan, 2014 1 commit
    • Andrei Paskevich's avatar
      WhyML: add "diverges", "reads {}", and "writes {}" effect clauses · 83858597
      Andrei Paskevich authored
      - "diverges" states that the computation may not terminate (which
        does not mean that is always diverges: just as any other effect
        annotation, this clause states a possibility of a side effect).
      - "reads {}" states that the computation does not access any variable
        except those that are listed elsewhere in the specification (or the
        proper function arguments, if "reads" is in a function spec).
      - "writes {}" states that the computation does not modify any mutable
      - If a function definition or an abstract computation may diverge,
        but there is no "diverges" clause in the specification, a warning
        is produced. If a function definition or an abstract computation
        always terminates, but there is a "diverges" clause in the spec,
        an error is produced.
      - If there is a "reads" or a "writes" clause in a function definition
        or an abstract computation, then every modified value must be listed
        in "writes" and every accessed external variable not mentioned in
        the spec must be listed in "reads". (Notice that this is a stricter
        requirement than before, when the presence of a "writes" clause
        did not require to specify "reads".) However, one does not have to
        write "reads {}" or "writes {}" if the corresponding lists are empty.
  8. 14 Jan, 2014 2 commits
  9. 03 Dec, 2013 1 commit
  10. 24 Nov, 2013 1 commit
  11. 22 Nov, 2013 1 commit
    • Andrei Paskevich's avatar
      WhyML: introduce "val ... in ..." construction · 7ecd3139
      Andrei Paskevich authored
      This is a syntactic sugar for higher-order "any", for which
      I can't find reasonably unambiguous syntax. One can write
        val x : int <spec> in <expr>
        val f (x : int) : int <spec> in <expr>
        val f <spec> (x : int) : int <spec> in <expr>
      for a function which is created via some effectful computation.
      This is a generalized form of top-level "val" which only admits
      latent effects (as in the second form above).
  12. 20 Nov, 2013 2 commits
  13. 19 Nov, 2013 6 commits
  14. 11 Nov, 2013 1 commit
  15. 10 Nov, 2013 2 commits
  16. 29 Oct, 2013 1 commit
    • Andrei Paskevich's avatar
      Term: do not store t_vars in terms · 7abeba05
      Andrei Paskevich authored
      we still keep bv_vars in the binders, so calculating the set
      of free variables only has to descend to the topmost binders.
      The difference on an example from BWare is quite striking:
      /usr/bin/time why3-replayer : with t_vars
      505.14user 15.58system 8:40.45elapsed 100%CPU (0avgtext+0avgdata 3140336maxresident)k
      /usr/bin/time why3-replayer : without t_vars
      242.96user 12.04system 4:16.31elapsed 99%CPU (0avgtext+0avgdata 2007184maxresident)k
      Not only we take 2/3 of memory, but we also gain in speed (less work
      for the GC, most probably).
      This patch should be tested on big WhyML examples,
      since src/whyml/mlw_*.ml are big users of t_vars.
      Thanks to Guillaume for the suggestion.
  17. 27 Oct, 2013 2 commits
    • Andrei Paskevich's avatar
      Typing: only accept opaqueness annotations in prototypes · 1c2e307c
      Andrei Paskevich authored
      TODO: impose the same restriction in programs
    • Andrei Paskevich's avatar
      accept untyped variables under quantifiers · 02fcd207
      Andrei Paskevich authored
      It is a matter of ongoing discussion how much type information we
      require from the user for the sake of readability of specification.
      Since types of quantified variables are important part of axioms
      and lemmas, we required them for the same reason we require the
      full prototypes for functions and predicates. However, when we
      typecheck program annotations, explicit types in quantifiers may
      quickly become an annoyance. Let's say, we define a polymorphic
      function "fn":
        let fn x y
          requires { forall z:'a. ... -> z = x }
        = ...
      Since in programs we [are going to] accept implicit type variables,
      the user may omit the types of "x" and "y", and they will be inferred
      by the typechecker. Now, if we are obliged to write the type of "z"
      in the postcondition, we cannot simply write 'a, because it will not
      unify with the implicit type of "x" (remember that programs are typed
      independently of specs). So, if we write the type of "z", we also have
      to write the type of "x". This is annoying and may even lead to errors
      if, by mistake, the user chooses 'a for the type of "x" and thus
      freezes 'a in all function definitions in "fn" while they were
      polymorphic in 'a till then.
      For this reason, it seems reasonable to accept untyped variables
      under quantifiers (DISCUSS: should we accept them only in specs?).
      However, we still require type variables in logic to be explicitly
      named (unless they come from the program, then they are accepted),
      and thus polymorphic axioms and lemmas would still have to have
      the explicitly typed quantified variables.
  18. 19 Oct, 2013 2 commits
  19. 28 Sep, 2013 1 commit
  20. 03 Aug, 2013 1 commit
  21. 27 May, 2013 1 commit
  22. 02 May, 2013 1 commit
  23. 25 Apr, 2013 1 commit
    • Andrei Paskevich's avatar
      whyml episode VI: the return of read effects · b4caa997
      Andrei Paskevich authored
      By popular demand, read effects are back. They serve to mark dependence
      of a program function on external variables which are otherwise not
      mentioned in the function's specification. Such annotation is necessary,
      for example, to add the needed type invariants.
      The "reads" clauses are comma-separated variables (contrary to write
      effects, where one must point out the modified field).
      If a user specifies a "reads" clause for a defined function, we check
      that every listed variable occurs in the code and that every free
      variable in the code occurs in the specification (which includes the
      "reads" clause). Notice that this concers function arguments, too:
        val r : ref int
        let f (x : ref int) reads {r} = x := !r
      would require x to be added to reads.
  24. 17 Apr, 2013 1 commit
  25. 07 Apr, 2013 1 commit
  26. 06 Apr, 2013 1 commit
  27. 23 Mar, 2013 1 commit