Skip to content
Snippets Groups Projects
abs 129 B
Newer Older
Bart Wijgers's avatar
Bart Wijgers committed
abs ( x : int | y : int ) {
    assume x > 0;
Bart Wijgers's avatar
Bart Wijgers committed
    if x < 0 then { y := 0 } else { skip; skip; skip; skip } ;
Bart Wijgers's avatar
Bart Wijgers committed
    assert y > 0
}