A simple program with no loop. {= x>0 =} { y=x ; z=y ; z++ ; z-- ; if (a>0) z++ else z-- ; } {= z>=0 =}
{= x>0 =} { y=x ; z=y ; z++ ; z-- ; if (a>0) z++ else z-- ; } {= z>=0 =}