• pure (can have loops and assignments, but no visible side effects – typically has a block (curly braces)

• strictpure - pure FP, val assignment, recursion allowed, conditional; convention is expression body not a block body. Main point: behind the scenes strictpure is transformed into a SMT function.

x = e;

is e has a mutable type then the assignment produces a copy

A(x = e, ....)   // constructor

copy of e if e is mutable type

m(x = e, ...) // method call

here we pass a reference to the object produced by e

the formal parameter to the method is always a “val” you cannot assign to it, but you can assign to components, and these changes are visible to the outside world.

• spec method

  • with no body @spec def bar(x: Z): Z = $

  • naming piece of a proof context (e.g., Lemma, or proof step)

  • naming invariant

• spec var