program abs {
           declarations
           post (y >= 0)
           subProgram abs(x -> Integer) -> Integer {
                                                  declarations
                                                  y -> Integer;
                                                  
statements
                                                  if(x < 0) then  {
                                                                 y := -x;
                                                                  }
                                                            else  {
                                                                 y := x;
                                                                  }
                                                  ;
                                                  return y;
                                                   };
           
statements
           skip;
            }