نشانهگذاری Z
نشانهگذاری Z یک زبان مشخصات رسمی است که برای توصیف و مدل سازی سیستمهای محاسباتی استفاده میشود. هدف آن توصیف مشخصات واضح از برنامههای کامپیوتری و بهطور کلی سیستمهای مبتنی بر کامپیوتر است.
تاریخچه
در سال ۱۹۷۴، جین-ریموند ابریل «معناشناسی داده» را منتشر کرد.[1] او از یک نماد استفاده کرد که بعدها تا پایان دهه ۱۹۸۰ در دانشگاه گرونوبل تدریس میشد، در حالی که در EDF (Électricité de France), ابریل یادداشتهای داخلی در Z نوشت. نشانهگذاری Z در سال ۱۹۸۰ در کتاب Méthodes de programmation استفاده شدهاست.[2]
Z در اصل در سال ۱۹۷۷ توسط ابریل با کمک استیو شومان و برتراند مایر پیشنهاد شد.[3] به علاوه آن در گروه برنامهنویسی تحقیقاتی در دانشگاه آکسفورد که ابریل در آن در اوایل دهه ۱۹۸۰ مشغول به کار بود توسعه یافت.
ابریل گفت: Z نام گرفتهاست "چون آن زبان نهایی است!"[4] اگر چه نام "Zermelo" نیز با نشانهگذاری Z مرتبط است زیرا از نظریه مجموعه Zermelo–Fraenkel استفاده میکند.
استفاده و نشانهگذاری
Z بر اساس استاندارد ریاضی نشانهگذاری است و در برهان نظریه مجموعه، حساب لامبدا، و اولین سفارش منطق گزارهها استفاده میشود. همه عبارات در نشانهگذاری Z تایپ میشوند در نتیجه از برخی از پارادوکسهای ساده و بی تکلف نظریه مجموعه اجتناب میشود. Z شامل کاتالوگ استاندارد شدهای (به نام جعبه ابزار ریاضی) از توابع ریاضی و گزارههایی است که توسط Z تعریف شدهاند.
اگر چه نشانهگذاری Z (درست مثل زبان APL، مدتها قبل از آن) از نمادهای غیر اسکی زیادی استفاده میکند، مشخصات شامل پیشنهادهایی برای ارائه نمادهای نشانهگذاری Z در اسکی و لاتکس است. همچنین رمزگذاری یونیکد برای تمامی نمادهای استاندارد Z وجود دارد.
استانداردها
ISO در سال ۲۰۰۲ تلاش استانداردسازی Z را تکمیل میکند. این استاندارد[5] و اصلاحیه فنی[6] از ISO به صورت رایگان در دسترس هستند:
- استاندارد در دسترس عموم است از ISO ITTF سایت رایگان و بهطور جداگانه در دسترس برای خرید از سایت ISO؛
- اصلاحیه فنی از سایت ISO به رایگان در دسترس است.
منابع
- Abrial, Jean-Raymond (1974), "Data Semantics", in Klimbie, J. W.; Koffeman, K. L., Proceedings of the IFIP Working Conference on Data Base Management, North-Holland, pp. 1–59
- Meyer, Bertrand; Baudoin, Claude (1980), Méthodes de programmation (به French), Eyrolles
- Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980), "A Specification Language", in Macnaghten, A. M.; McKeag, R. M., On the Construction of Programs, Cambridge University Press, ISBN 0-521-23090-X (describes early version of the language).
- Hoogeboom, Hendrik Jan. "Formal Methods in Software Engineering" (PDF). The Netherland: University of Leiden. Retrieved 14 April 2017.
- "ISO/IEC 13568:2002". Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (Zipped PDF). ISO. 2002-07-01. 196 pp.
- "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.
- 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 نماد اظهارات و توضیح