From Wikipedia, the free encyclopedia.
Z is a problem specification language rather than a computer programming language as such. It is used to formalise an algorithm that might otherwise remain loosely defined, and thereby to verify the correctness of that algorithm by the analyst prior to having that algorithm programmed in a computer programming language by a programmer.

