In section 2, we introduce U-topological lattices that is complete lattices endowed with a U-topology. The continuity of functions is characterized in this topology and fixed point theorems are recalled in this context.

   The semantics of recursive procedures is defined by a predicate transformer associated with the procedure. This predicate transformer is the least fixed point of a system of functional equations (§3.2) associated with the procedure by a syntactic algorithm (§3.1).

   In section 4, we study the mechanized discovery of approximate properties of recursive procedures. The notion of approximation of a semantic property is introduced by means of a closure operator on the U-topological lattice of prediactes. Several characterizations of closure operations are given which can be used in practice to defined the approximate properties of interest (§4.1.1). The lattice of closure operators induces a hierarchy of program analyzes according to their fineness. Combinations of different analyzes are studied (§4.1.2). A closure operator defined on the semantic U-topological space induces a relative topology on the complete lattice of approximate properties, so that the space of approximate properties is a U-topological lattice (§4.1.3). Then functions and functionals on the space of semantic properties can be expressed in the space of approximate properties (§4.1.4, §4.1.5). In order to represent the space of approximate properties in a machine we use an homeomorphic space the elements of which can be represented inside a computer (§4.1.6). The systematic correspondence between semantic and approximate properties of programs, allows the association of a system of approximate functional equations with a recursive procedure (§4.1.7). Its mechanical resolution by successive approximations determines an approximate predicate transformer which is a partial representation of the meaning of the procedure (§4.2). In practice chaotic iterations are used to construct this solution when the space of approximate properties is finite (§4.2.1) but when infinite strengthened chaotic iterations must be used to accelerate the convergence (§4.2.2).

   Throughout the paper various practical examples are given.

\bibitem{CousotCousot77-3}
P{.} Cousot and R{.} Cousot.
\newblock Static determination of dynamic properties of recursive
procedures.
\newblock In \emph{IFIP Conf{.} on Formal Description of Programming
Concepts, St-Andrews, N.B., CA}, E.J{.} Neuhold (Ed.), pages 237--277,
St-Andrews, N.B., Canada, 1977.  North\discretionary{-}{}{-}Holland
Publishing Company (1978).

@inProceedings{CousotCousot77-3,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Static determination of dynamic properties of recursive 
                procedures},
   pages =     {237--277},
   editor =    {Neuhold, E.J{.}},
   booktitle = {IFIP Conf{.} on Formal Description of Programming Concepts, 
                St-Andrews, N.B., CA},
   publisher = {North\discretionary{-}{}{-}Holland},
   year =      1977,
}