program abs {
           declarations
           pre (valid_index(t,i) && valid_index(t,j)); 
           post ((t[i] == old(t[j])) && (t[j] == old(t[i])))
           subProgram swap(t -> Array[10],i -> Integer,j -> Integer) -> Array[10] {
                                                                                 declarations
                                                                                 tmp -> Integer;
                                                                                 
statements
                                                                                 tmp := t[i];
                                                                                 t[i] := t[j];
                                                                                 t[j] := tmp;
                                                                                 return t;
                                                                                  };
           
statements
           skip;
            }