VAOL, chapter 9 (Correctness), page 124

     An Old expression of the form old e, where `e' is  an
     expression  of  type `TE', is valid if and only if it
     satisfies the following two conditions:

        1 It  appears  in  a  Postcondition  clause  of  a
          Routine `r'.

        2 Transforming `r' into  a  function  with  result
          type  `TE'  (by  adding  a result type if `r' is
          procedure, or changing its result type if it  is
          already  a  function)  and  replacing its entire
          Routine part by
            do
              Result := e
            end
          would yield a valid routine.