Bevezetés
A Z nyelv amit Zermelo-Fraenkel halmazelméletéről neveztek el egy formális specifikációs nyelv számítógépes rendszerek modellezésére és leírására.A Z nyelv az általános matematikai jelöléseket használja az axiómatikus halmazelméletből, a lambda kalkulusból és az elsőrendű predikátum logikából.Minden kifejezés típusos így kerülve ki néhány paradoxont ami a halmazelméletből származik.A nyelvhez tartozik még egy általánosított katalógus (egy matematikai eszköztár) ami általános matematikai függvényeket és predikátumokat tartalmaz.2002-ben befejezték a Z ISO-szabványosítását.