Vickers, TrevorMorgan, Carroll2003-07-102004-05-192011-01-052004-05-192011-01-051994http://hdl.handle.net/1885/40782http://digitalcollections.anu.edu.au/handle/1885/40782Invariants allow a rigorous treatment of types as sets in the refinement calculus, a method for developing imperative programs. The interaction of procedures and invariants is explored, resulting in a practical formalisation of existing programming practice.177006 bytes356 bytesapplication/pdfapplication/octet-streamen-AUrefinement calculusimperative programsinvariant semanticsenvironment semantics1994