Z Notation
Z is the “ultimate language” as stated by Jean-Raymond Abrial who invented this formal specification language in 1977. This language aims for a precise and clear specification of computer-based systems based on the Zermelo-Fraenkel set theory, lambda calculus, and first-order predicate logic. The main elements of Z are so-called “schemata” that consist of typed variables and constraints on the assignment of these. Z provides a standardized catalogue of often used mathematical functions and predicates.