abs

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