1. 14 Oct, 2018 1 commit
  2. 28 Sep, 2018 1 commit
    • Raphael Rieu-Helft's avatar
      Add support for partial functions · 17ed1270
      Raphael Rieu-Helft authored
      Program functions can be declared as partial with "let/val partial".
      Similarly to "diverges", partial code cannot be ghost, however it does not need to be
      explicitly specified as partial.
      
      Fixes #184.
      17ed1270
  3. 14 Jun, 2018 1 commit
  4. 13 Dec, 2017 1 commit
  5. 16 Jun, 2017 1 commit
    • Andrei Paskevich's avatar
      WhymL: break and continue · df239061
      Andrei Paskevich authored
      Without an argument, break and continue refer to the innermost loop.
      A label put over an expression sequence starting with a loop, can be
      used as an optional argument for break and continue:
      
        label L in
        [ghost] ["tag"] [M.begin]
          while true do
            ...
            break L
            ...
          done;
          [...]
        [end] [: unit]
      
      In the square brackets are listed the constructions allowed between
      the label declaration and the loop expression.
      df239061
  6. 08 Jun, 2017 1 commit
  7. 06 Jun, 2017 1 commit
  8. 04 Jun, 2017 1 commit
  9. 29 Mar, 2017 1 commit
  10. 30 Dec, 2016 1 commit
    • Andrei Paskevich's avatar
      slightly change coloring · 2fbef962
      Andrei Paskevich authored
      - builtin Why3 connectors and parens are "Operator", not "Keyword"
      - square brackets are Normal (just like other used-defined ops)
      2fbef962
  11. 18 Oct, 2016 2 commits
    • Andrei Paskevich's avatar
      vim-pathogen compliance · 7908605b
      Andrei Paskevich authored
      To install the Why3-related Vim files, just create a symbolic link:
        ln -s "$(why3 --print-datadir)/vim" ~/.vim/bundle/why3
      
      Thanks to Johanness Kanig for the suggestion.
      7908605b
    • Andrei Paskevich's avatar
      vim-pathogen compliance · 36add616
      Andrei Paskevich authored
      To install the Why3-related Vim files, just create a symbolic link:
        ln -s "$(why3 --print-datadir)/vim" ~/.vim/bundle/why3
      
      Thanks to Johanness Kanig for the suggestion.
      36add616
  12. 01 Apr, 2016 1 commit
  13. 10 Dec, 2015 1 commit
  14. 02 Jul, 2015 1 commit
  15. 14 Feb, 2014 1 commit
    • 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).
      4fd8b24d
  16. 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
        value.
      
      - 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.
      83858597
  17. 05 Nov, 2012 1 commit
  18. 12 Oct, 2012 1 commit
  19. 23 Jun, 2012 1 commit
  20. 22 May, 2012 1 commit
  21. 17 Mar, 2012 1 commit
  22. 11 Mar, 2012 1 commit