Z 표기법
Z notation
Z 표기법 /zzdd/는 컴퓨팅 [1]시스템을 기술 및 모델링하기 위해 사용되는 공식 사양 언어입니다.일반적으로 컴퓨터 프로그램 및 컴퓨터 기반 시스템의 명확한 사양을 목표로 합니다.
역사
1974년, 장 레이몬드 애브리얼은 "데이터 의미론"[2]을 출판했다.그는 후에 1980년대 말까지 그르노블 대학에서 가르칠 표기법을 사용했다.EDF(Electricité de France)에서 Bertrand Meyer와 함께 일하는 동안 Abrial은 [3]Z 개발에도 종사했습니다.Z 표기법은 1980년 출판된 Methodes de programmation에서 [4]사용됩니다.
Z는 원래 1977년 Abrial에 의해 Steve Schuman과 Bertrand [5]Meyer의 도움으로 제안되었다.그것은 1980년대 초에 Abrial이 일했던 Oxford 대학의 Programming Research Group에서 1979년 9월에 Oxford에 도착했다.
Abrial은 비록 "Zermelo"라는 이름이 또한 Zermelo-Fraenkel 집합론의 사용을 통해 Z 표기법과 연관되어 있지만, Z는 "최종 언어이기 때문에!"[6]라는 이름이 붙여졌다고 말했다.
사용법 및 표기법
Z는 공리 집합론, 람다 미적분, 1차 술어 [7]논리에 사용되는 표준 수학 표기법에 기초합니다.Z 표기의 모든 표현은 타이핑되므로, 순진한 집합론의 역설 중 일부를 피할 수 있습니다.Z에는 일반적으로 사용되는 수학 함수 및 술어의 표준화된 카탈로그(수학적 툴킷이라고 함)가 포함되어 있으며, Z 자체를 사용하여 정의됩니다.표준 논리 연산자를 기반으로 자체 연산자를 사용하여 결합할 수 있고 다른 스키마에 스키마를 포함시킴으로써 결합할 수 있는 Z 스키마 박스와 함께 증강됩니다.이를 통해 Z사양을 큰사양으로 편리하게 구축할 수 있습니다.
Z 표기법(APL 언어와 마찬가지로 훨씬 이전)은 많은 비 ASC를 사용합니다.II 기호, 사양은 ASCII 및 LaTeX에서 Z 표기 기호를 렌더링하기 위한 제안을 포함합니다.또한 모든 표준 Z [8]기호를 위한 유니코드 인코딩도 있습니다.
표준
ISO는 2002년에 Z 표준화 작업을 완료했습니다.이[9] 표준 및 기술 코리젠드는[10] ISO 프리에서 구할 수 있습니다.
상
1992년, 옥스퍼드 대학 컴퓨팅 연구소는 Z [11]표기의 IBM과 공동 개발한 공로로 퀸즈 테크니컬 어워드(Queen's Technical Achievement)를 수상했습니다.
「 」를 참조해 주세요.
- Z 사용자 그룹(ZUG)
- Community Z Tools(CZT) 프로젝트
- 기타 공식 방법(및 공식 사양을 사용하는 언어):
- Fastest는 Z 표기법에 대한 모델 기반 테스트 도구입니다.
레퍼런스
- ^ Bowen, Jonathan P. (2016). "Z notation: Whence the cause and whither the course?". Engineering Trustworthy Software Systems. Lecture Notes in Computer Science. Vol. 9506. Springer. pp. 103–151. doi:10.1007/978-3-319-29628-9_3.
- ^ Abrial, Jean-Raymond (1974), "Data Semantics", in Klimbie, J. W.; Koffeman, K. L. (eds.), Proceedings of the IFIP Working Conference on Data Base Management, North-Holland, pp. 1–59
- ^ Hoare, Tony (2010). "Greetings to Bertrand on the Occasion of his Sixtieth Birthday" (PDF). The Future of Software Engineering. Springer. p. 183. ISBN 978-3-642-15187-3.
- ^ Meyer, Bertrand; Baudoin, Claude (1980), Méthodes de programmation (in French), Eyrolles
- ^ Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980), "A Specification Language", in Macnaghten, A. M.; McKeag, R. M. (eds.), On the Construction of Programs, Cambridge University Press, ISBN 0-521-23090-X (초기 버전의 언어 참조).
- ^ Hoogeboom, Hendrik Jan. "Formal Methods in Software Engineering" (PDF). The Netherland: University of Leiden. Retrieved 14 April 2017.
- ^ Spivey, J. Michael (1992). The Z Notation: A Reference Manual. International Series in Computer Science (2nd ed.). Hemel Hempstead: Prentice Hall. ISBN 978-0139785290.
- ^ Korpela, Jukka K. "Unicode Explained: Internationalize Documents, Programs, and Web Sites". unicode-search.net. Retrieved 24 March 2020.
- ^ a b c "ISO/IEC 13568:2002". Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (Zipped PDF). ISO. 1 July 2002. 196 페이지
- ^ a b "ISO/IEC 13568:2002/Cor.1:2007". Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics — Technical corrigendum 1 (PDF). ISO. 15 July 2007. 12pp.
- ^ "The Queen's Award for Technological Achievement 1992". Oxford University Computing Laboratory. Archived from the original on 22 March 2012. Retrieved 17 October 2021.
추가 정보
- Spivey, John Michael (1992). The Z Notation: A reference manual. International Series in Computer Science (2nd ed.). Prentice Hall.
- Davies, Jim; Woodcock, Jim (1996). Using Z: Specification, Refinement and Proof. International Series in Computer Science. Prentice Hall. ISBN 0-13-948472-8.
- Bowen, Jonathan (1996). Formal Specification and Documentation using Z: A Case Study Approach. International Thomson Computer Press, International Thomson Publishing. ISBN 1-85032-230-9.
- Jacky, Jonathan (1997). The Way of Z: Practical Programming with Formal Methods. Cambridge University Press. ISBN 0-521-55976-6.
