Posets, Lattices, and Categories

Abstract

This chapter introduces the central mathematical structures that are needed to formalize the refinement calculus: partially ordered sets (posets), lattices, and categories. We identify the basic properties of posets and lattices, and use them for a classification of lattices. We also show how to construct new lattices out of old ones as Cartesian products and function spaces. We study structure-preserving mappings (homomorphisms) on lattices. Finally, we show how to form a certain kind of category out of these lattices. The simple notions identified in this chapter underlie the formal reasoning about properties of programs, specifications, and contracts in general.