A Specification Language used for describing and modelling computing systems. Predominant in Zermello-Frankel Set Theory.