DATA REFINEMENT IN A CATEGORICAL SETTING

Abstract

Data refinement is one of the most effective formal methods for design and development of large programs and systems [6, 8, 11, 12, 15]. Design starts with a grtapg D, whose nodes are names b, c, .., d of basic types and whose arrows are the names p. q, .., r of primitive operations on values of the type. We introduce the notation p to stand for the source node of p in D, and P for the target node. A program text over graph D in a language L is the text of any syntactically valid and strictly typed program whose primitive types and operations are named by objects and arrows from the graph D. There are assembled into a program by means of the constructors of the language L.