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

Question

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?

Answer

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