An Outline Pattern Language for Z: Five Illustrations and Two Tables

摘要

We introduce a pattern language for using formal methods in computer system engineering. We focus on the Z notation, but many of the patterns are adaptable to other formal notations, or can be used to help choose a notation, or to decide on a style of formality. As in other pattern languages, we are providing a new presentation of existing practice, to make it accessible to computer systems engineering. We propose an initial classification of Z patterns, present selected examples, and outline issues of tool support.