Invariants and well-foundedness in program algebra

Program algebras abstract the essential properties of programming languages in the form of algebraic laws. The proof of a refinement law may be expressed in terms of the algebraic properties of programs required for the law to hold, rather than directly in terms of the semantics of a language. This has the advantage that the law is then valid for any programming language that satisfies the required algebraic properties. By characterised the important properties of programming languages algebraically we can devise simple proofs of common refinement laws. In this paper we consider standard refinement laws for sequential programs. We give simple characterisations of program invariants and well foundedness of statements