We present here a framework to prove input/output properties {p} S {q}. It is based on the search for a program invariant, very much as in the proof of a while-loop in Hoare's logic. Our main result is the completeness of the method: for any valid property, there exists an invariant to prove it. In fact, this invariant is nothing but the logical encoding of all data-flow dependencies specified by the program. Its external from is actually exactly the same as the program text, up to a suitable interpretation of the ``='' sign. Of course, a property may also be proved using weaker ad-hoc invariants.
Using this approach sets up a firm foundation for all kinds of ``handwaving'' manipulations found in the literature about Alpha programs. It is especially crucial when the properties under study cannot be expressed as another Alpha program: non-linear indexing of arrays, induction arguments, etc.
@TECHREPORT{LIP:RR95-08, AUTHOR = {Luc Bougé and David Cachera}, INSTITUTION = {LIP, ENS Lyon, France}, NUMBER = {RR96-32}, TITLE = {A logical framework for proving Alpha programs}, TYPE = {Research Report}, YEAR = {1996}, URL = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR96/RR96-32.ps.Z} }