Procedures and invariants in the refinement calculus
Invariants 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.
|Collections||ANU Research Publications|
|TR-CS-94-04.pdf||172.86 kB||Adobe PDF|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.