Due punti di tipo della notazione Z

Dichiara quale genere di valore può assumere una variabile. Z usa insiemi e logica per descrivere con precisione dati e regole di un sistema. In una dichiarazione, il nome precede ⦂ e un’espressione che indica un insieme lo segue. L’insieme limita i valori ammessi e determina il tipo della variabile.

Per esempio, x ⦂ ℤ dichiara x come numero intero: ℤ è l’insieme degli interi, compresi quelli negativi e lo zero. Non assegna un numero specifico a x e non esegue un calcolo.

Z nacque dal lavoro di Jean-Raymond Abrial alla fine degli anni Settanta e fu sviluppato ulteriormente a Oxford. Molti testi Z usano i normali due punti : nelle dichiarazioni. Il carattere dedicato ⦂ non introduce una regola matematica diversa, ma un programma non tratta necessariamente i due caratteri come intercambiabili.