Is there any difference between a method without a modifies clause and a function method with a reads this clause? I know that the latter you can use in expressions. Is there anything the former can do that the latter can’t, for example?


Compared to a function, a method can

  • allocate objects and arrays (new)
  • use non-determinism
  • use loops
  • have multiple outputs
  • read anything in the heap