Proving Program Properties Specified with Subtype Marks

摘要

This paper presents a method that facilitates formal reasoning about the correctness of programs. In this method, properties of programs (e.g. pre- and postconditions of functions) are described in terms of type invariants. Subtype marks are annotations attached to types and denote type invariants. A large amount of program properties expressed with subtype marks are verifiable fully automatically by an appropriate type system; the rest can be proven with a proof system. In this paper an eager pure functional language with a type system supporting subtype marks is briefly described. By assigning an interpretation to subtype marks, a concept of program correctness is introduced. The soundness of the presented type system is investigated.