In section 2 we establish the lattice theoretic foundations upon which the synthesis of invariant assertions is based. We study the resolution of a fixpoint system of equations by Jacobi's successive approximation method. Under continuity hypothesis we show that any chaotic iterative method converges to the optimal solution. In section 3 we study the deductive semantics of programs. We show that a system of logical forward equations can be associated with a program using the predicate transformer rules which define the semantics of elementary instructions. The resolution of this system of semantic equations by chaotic iterations leads to the optimal invariants which exactly define the semantics of this program. Therefore the optimal invariants can be used for total correctness proffs (section 4). Next we show that usually a system of inequations is used as a substitute for the system of equations. Hence the solutions to this system of inequations are approximate invarians which can only be used for proofs of partial correctness (section 5). In section 6 we show that symbolic execution of programs concists in fact in solving the semantic equations associated with this program. The constrcution of the symbolic execution tree corresponds to the chaotic successive approximations method. Therefore symbolic execution permits optimal invariants to be discovered provided that one can pass to the limit, that is consider infinite paths in the symbolic execution tree. Induction principles can be used for that purpose. In section 7 we show that an approximation of the optimal solution to a fixpoint system of equations can be obtained by strenghthening the term of a chaotic iteration sequence. This formalizes the synthesis of approximate invariants by heuristic methods. Various examples provide a helpful intuitive support to the technical sections.

• The word optimal would have better been chosen as strongest (most precise);
• The word eventually is used with its french meaning of a possibility (may be true) whereas in english it means a certainty (must be true).
• The proof of theorem 2.2 is erroneous. A generalization to asynchronous iterations and a correct proof was later published in IMAG research report R.R. 88;

\bibitem{CousotCousot77-2}
P{.} Cousot and R{.} Cousot.
\newblock Automatic synthesis of optimal invariant assertions: mathematical
          foundations.
\newblock In {\em ACM Symposium on Artificial Intelligence \& Programming
          Languages}, Rochester, New York, ACM SIGPLAN Notices{} 12(8):1--12, 
          August 1977.

@inproceedings{CousotCousot77-4,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Automatic synthesis of optimal invariant assertions: mathematical
                foundations},
   booktitle = {ACM Symposium on Artificial Intelligence \& Programming Languages},
   address =   {Rochester, NY, ACM SIGPLAN Not{.}{} 12(8):1--12},
   month =     aug,
   year =      1977,
}

@Article{Cousot:1977:ASO,
  author =       "P. Cousot and R. Cousot",
  title =        "Automatic synthesis of optimal invariant assertions:
                 mathematical foundations",
  journal =      j-SIGPLAN,
  volume =       "12",
  number =       "8",
  pages =        "1--12",
  month =        aug,
  year =         "1977",
  CODEN =        "SINODQ",
  ISSN =         "0362-1340",
  bibdate =      "Sat Apr 25 11:46:37 MDT 1998",
  acknowledgement = ack-nhfb,
  classification = "C4240 (Programming and algorithm theory)",
  conflocation = "Rochester, NY, USA; 15-17 Aug. 1977",
  conftitle =    "ACM Symposium in Artificial Intelligence and
                 Programming Languages",
  corpsource =   "Univ. of Sci. and Medicale, Grenoble, France",
  keywords =     "automatic programming; automatic synthesis; optimal
                 invariant assertions; programming theory; programs",
  sponsororg =   "ACM",
  treatment =    "T Theoretical or Mathematical",
}