• Patrick Cousot & Radhia Cousot.
Static determination of dynamic properties of recursive procedures.
In IFIP Conference on Formal Description of Programming Concepts, E.J. Neuhold, (Ed.), pages 237—277, St-Andrews, N.B., Canada, 1977. North-Holland Publishing Company (1978).

• Introduction:    We present a general technique for determining properties of recursive procedures. For example, a mechanized analysis of the procedure reverse can show that whenever L is a non-empty linked linear list then reverse(L) is a non-empty linked linear list which shares no elements with L. This information about reverse approximates the fact that reverse(L) is a reversed copy of L.

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,
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,
}