Z (pronounced zed) is a set of conventions for presenting mathematical text, chosen to make it convenient to use simple mathematics to describe computing systems. I say computing systems because Z has been used to model hardware as well as software.
Z is a model-based notation. In Z you usually model a system by representing its state -- a collection of state variables and their values -- and some operations that can change its state. A model that is characterized by the operations it describes is called an abstract data type (ADT). This modelling style is a good match to imperative, procedural programming languages that provide a rich collection of data types, and also to some physical systems (such as digital electronics) that include storage elements. Z is also a natural fit to object-oriented programming. Z state variables are like instance variables and the operations are like methods; Z even provides a kind of inheritance. However, Z is not limited just to ADT's and object-oriented style; you can also use Z in a functional style, among others.
Z dictates few assumptions about what can be modelled. Z is just a notation, it is not a method; the Z notation can support many different methods. The meaning of a Z text is determined by its authors. It can be understood to model only the behavior of a system: it is an abstract formal specification. Or, the elements of a Z text can be understood to represent structures in code: modules, data types, procedures, functions, classes, objects. In that case the Z model is a detailed design.
Z is not an executable notation. In general, Z specifications cannot be interpreted or compiled into a running program (or prototype or simulation). Z is not a programming language. Z texts are not just programs written in very high-level language. What would be the point of writing the program twice?
Z was designed for people, not machines. For years Z was exclusively a pencil-and-paper notation. Z encourages a style where formulas are annotated liberally with prose. Z documents usually include more prose than formal text. Novices can be intimidated by the appearance of Z: a mixture of boxes, text, Greek letters, and invented pictorial symbols. But the notation is easy to learn; once assimilated, its advantages become clear. The boxes and pictorial symbols in Z help your eye grasp the structure of the model even before you read it.
Z actually includes two notations. The first is the notation of ordinary discrete mathematics. The second notation provides structure to the mathematical text: it provides several structuring constructs called paragraphs. The most conspicuous kind of Z paragraph is a macro-like abbreviation and naming construct called the schema. Z defines a schema calculus you can use to build big schemas from small ones. The schema is the feature that most distinguishes Z from other formal notations.
The mathematical notation of Z consists of a small core, supplemented by a larger collection of useful objects and operators called the Z mathematical tool-kit. The tool-kit is not software, it is a collection of mathematical theories: definitions and laws concerning objects such as sets, tuples, relations, functions, sequences and their operators. In Z we use these mathematical objects to model data structures and other components of computing systems. The tool-kit plays somewhat the same role in Z that a standard library of types and functions does in an executable programming language.
Z is supported by tools. The notation is defined with sufficient precision that Z texts can be processed by machine. Software tools are available for writing and displaying the special Z symbols and typesetting documents, for checking Z texts for syntax and type errors in much the same way that a compiler checks code in an executable programming language, and even for assisting in proving claims about the behavior of systems modelled in Z. These tools are invaluable for serious work, but you do not need them to begin learning and using Z.
Z is a mature notation. Conceived in the late 1970's, it developed through the 1980's in collaborative projects between Oxford University and industrial partners including IBM and Inmos (a semiconductor producer). The first Z reference manual to be widely published benefited from this long experience when it finally appeared in 1989. An international Z standard was completed in 2002. Z has served as the basis for other notations, including several variants adapted for object-oriented programming.
From chapter 4 in The Way of Z
Links to some Z examples
Other pages about Z and formal methods