abs ( x : int | y : int ) { assume x > 0;
if x < 0 then { y := 0 } else { skip; skip; skip; skip } ;
assert y > 0 }