Z명세 

타입이 있는 집합 이론과 논리 EX) 집합, 관계, 함수, 술어 논리(predicate logic)사용