program abs {
           declarations
           post ((result >= x) && (result >= y)); 
           post forall(z -> Integer): ((z >= x) && ((z >= y) => (z >= result)))
           subProgram max(x -> Integer,y -> Integer) -> Integer {
                                                               declarations
                                                               z -> Integer;
                                                               
statements
                                                               if(x > y) then  {
                                                                              z := y;
                                                                               }
                                                                         else  {
                                                                              z := x;
                                                                               }
                                                               ;
                                                               return z;
                                                                };
           
statements
           skip;
            }