\programVariables {
   int i;
}
\problem {
   \forall int il; 
   {i:=il} 0 <= i -> (( \<{while (i>0) i--;}\> i=0)))
}