• 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
mlw_tree.ml 6.31 KB