4.4. Assignment and update operators🔗

Assignment targets a local or a field. A multi-assignment unpacks a call with several outputs; its right-hand side must be such a call, and its targets are positional. A target introduced with var declares a new local, and a bare target updates an existing one.

procedure triple() returns (a: int, b: int, c: int)
  opaque
{
  a := 1; b := 2; c := 3
};

composite Holder { var field: int }

procedure assignments()
  opaque
{
  var x: int := 3;
  var obj: Holder := new Holder;
  obj#field := 4;
  assign var p: int, x, var r: int := triple();
  assert p == 1
};

The Java-style increment and compound-assignment forms are also available. The prefix forms yield the new value and the postfix forms the old one:

procedure updateOperators()
  opaque
{
  var x: int := 0;
  ++x;
  x++;
  --x;
  x--;
  x += 2;
  var s: string := "pre";
  s ^= "suffix";
  assert x == 2
};

Each compound form means what it looks like: x op= y is x := x op y. Increment and decrement are currently restricted to int and to constrained types over int. Both families accept a field lvalue, but an update operator on a field duplicates the receiver expression, so keep the receiver side-effect-free — bind it to a local first if it is not.