نشانه‌گذاری Z

یک مثال از یک مشخصات رسمی (به زبان اسپانیایی) با استفاده از نشانه‌گذاری Z.

نشانه‌گذاری Z یک زبان مشخصات رسمی است که برای توصیف و مدل سازی سیستم‌های محاسباتی استفاده می‌شود. هدف آن توصیف مشخصات واضح از برنامه‌های کامپیوتری و به‌طور کلی سیستم‌های مبتنی بر کامپیوتر است.

تاریخچه

در سال ۱۹۷۴، جین-ریموند ابریل «معناشناسی داده» را منتشر کرد.^[۱] او از یک نماد استفاده کرد که بعدها تا پایان دهه ۱۹۸۰ در دانشگاه گرونوبل تدریس می‌شد، در حالی که در EDF (Électricité de France), ابریل یادداشت‌های داخلی در Z نوشت.^{[نیازمند منبع]} نشانه‌گذاری Z در سال ۱۹۸۰ در کتاب Méthodes de programmation استفاده شده‌است.^[۲]

Z در اصل در سال ۱۹۷۷ توسط ابریل با کمک استیو شومان و برتراند مایر پیشنهاد شد.^[۳] به علاوه آن در گروه برنامه‌نویسی تحقیقاتی در دانشگاه آکسفورد که ابریل در آن در اوایل دهه ۱۹۸۰ مشغول به کار بود توسعه یافت.

ابریل گفت: Z نام گرفته‌است "چون آن زبان نهایی است!"^[۴] اگر چه نام "Zermelo" نیز با نشانه‌گذاری Z مرتبط است زیرا از نظریه مجموعه Zermelo–Fraenkel استفاده می‌کند.

استفاده و نشانه‌گذاری

Z بر اساس استاندارد ریاضی نشانه‌گذاری است و در برهان نظریه مجموعه، حساب لامبدا، و اولین سفارش منطق گزاره‌ها استفاده می‌شود. همه عبارات در نشانه‌گذاری Z تایپ می‌شوند در نتیجه از برخی از پارادوکس‌های ساده و بی تکلف نظریه مجموعه اجتناب می‌شود. Z شامل کاتالوگ استاندارد شده‌ای (به نام جعبه ابزار ریاضی) از توابع ریاضی و گزاره‌هایی است که توسط Z تعریف شده‌اند.

اگر چه نشانه‌گذاری Z (درست مثل زبان ای‌پی‌ال، مدت‌ها قبل از آن) از نمادهای غیر اسکی زیادی استفاده می‌کند، مشخصات شامل پیشنهادهایی برای ارائه نمادهای نشانه‌گذاری Z در اسکی و لاتکس است. همچنین رمزگذاری یونیکد برای تمامی نمادهای استاندارد Z وجود دارد.

استانداردها

سازمان بین‌المللی استانداردسازی در سال ۲۰۰۲ تلاش استانداردسازی Z را تکمیل می‌کند. این استاندارد^[۵] و اصلاحیه فنی^[۶] از ISO به صورت رایگان در دسترس هستند:

• استاندارد در دسترس عموم است از ISO ITTF سایت رایگان و به‌طور جداگانه در دسترس برای خرید از سایت ISO؛
• اصلاحیه فنی از سایت ISO به رایگان در دسترس است.

منابع

1. 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
2. Meyer, Bertrand; Baudoin, Claude (1980), Méthodes de programmation (به فرانسوی), Eyrolles
3. 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 (describes early version of the language).
4. Hoogeboom, Hendrik Jan. "Formal Methods in Software Engineering" (PDF). The Netherland: University of Leiden. Retrieved 14 April 2017.
5. "ISO/IEC 13568:2002". Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (Zipped PDF). ISO. 2002-07-01. 196 pp.
6. "ISO/IEC 13568:2002/Cor.1:2007". Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics — Technical corrigendum 1 (PDF). ISO. 2007-07-15. 12 pp.

برای مطالعهٔ بیشتر

• Spivey, John Michael (1992). The Z Notation: A reference manual. International Series in Computer Science (2nd ed.). Prentice Hall. Archived from the original on 9 October 2008. Retrieved 29 November 2017.
• Davies, Jim; Woodcock, Jim (1996). Using Z: Specification, Refinement and Proof. International Series in Computer Science. Prentice Hall. ISBN 0-13-948472-8. Archived from the original on 27 June 2009. Retrieved 29 November 2017.
• Bowen, Jonathan (1996). Formal Specification and Documentation using Z: A Case Study Approach. International Thomson Computer Press. ISBN 1-85032-230-9. Archived from the original on 4 March 2017. Retrieved 29 November 2017.
• Jacky, Jonathan (1997). The Way of Z: Practical Programming with Formal Methods. Cambridge University Press. ISBN 0-521-55976-6.

پیوند به بیرون

• Toyn, Ian, Z Specification proposals, UK: York, archived from the original on 22 June 2012, retrieved 29 November 2017.
• WSDL 2.0, W3Cیک حاوی مشخصات Z نماد اظهارات و توضیح