نشانهگذاری 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 به صورت رایگان در دسترس هستند: