Multiple Assignment
Multiple assignment has the form
x1, x2, x3, …, xn := e1, e2, e3, …, en
where xi are distinct simple variables and ei are expressions.
wp(x1, x2, x3, …, xn := e1, e2, e3, …, en, R)
= domain(e1, e2, e3, …, en) cand R e1, e2, e3, …, en x1, x2, x3, …, xn
Examples: x,y := y, x;
x,y,z := y,z,x
wp(z,y:=z*x, y-1, y>=0 ? z*xy = c)