Program Specification and Data Refinement in Type Theory

Zhaohui Luo

Abstract: We develop a type-theoretic approach to program specification and data refinement and show that a type theory with a strong logical power and nice structural mechanisms provides an adequate formalism for modular development of programs and specifications. Specification of abstract data types is considered and a notion of abstract implementation between specifications is defined in the type theory and studied as a basis for correct and modular development of programs by stepwise refinement. The higher-order structural mechanisms in the type theory provide useful and flexible tools (specification operations and parameterized specifications) for modular design and structured specification. Refinement maps (programs and design decisions) and proofs of implementation correctness can be developed by means of the existing proof development systems based on type theories.

LFCS report ECS-LFCS-91-131

Previous | Index | Next