use int.Int (** three global mutable variables *) val ref x : int val ref y : int val ref z : int (** computes the maximum of `x` and `y` and stores the result in `z` *) let compute_max_x_y_in_z () requires { true } ensures { z = x \/ z = y } ensures { z >= x /\ z >= y } = if x <= y then z <- y else z <- x (** computes the half of `x` (very inefficiently) stores the result in `y` *) let compute_half_of_x () requires { x >= 0 } ensures { 2*y = x \/ 2*y+1 = x } = y <- 0; while 2*(y+1) <= x do y <- y+1 done