Z notasyonu

Z notasyonu İngilizce telaffuz: [ z ɛ d], bilgi işlem sistemlerini tanımlamak ve modellemek için kullanılan bir tanımla dilinin resmi notasyonudur. Genel olarak bilgisayar programı ve bilgisayar tabanlı sistemlerin belirtilmesi hedeflenmektedir.

Z notasyonunu kullanarak formal specification (İspanyolca'da) örneği

Tarihi

1974'te Jean-Raymond Abrial "Veri Semantiği"ni yayınladı.^[1] Daha sonra 1980'lerin sonuna kadar Grenoble Üniversitesi'nde öğretilecek bir notasyon kullandı. Abrial EDF'deyken Abrial, Z'ye ilişkin iç notlar yazdı. Z notasyonu, 1980 tarihli "Méthodes de programmation" kitabında kullanılmıştır.^[2]

Z ilk olarak 1977'de Abrial tarafından Steve Schuman ve Bertrand Meyer'in yardımıyla ileri sürüldü.^[3] Abrial'in 1980'lerin başında çalıştığı, Eylül 1979'da Oxford'a geldiği Programlama Araştırma Grubu'nda Oxford Üniversitesi'nde geliştirildi.

Araçlar

• Community Z Tools (CZT) (project), Source forge, 1 Temmuz 2004 tarihinde kaynağından arşivlendi, erişim tarihi: 3 Mart 2017.
• Z Word tools (project), Source forge, 24 Mart 2017 tarihinde kaynağından arşivlendi, erişim tarihi: 3 Mart 2017 for developing and checking Z specifications in Microsoft Word.
• Spivey, Michael ‘Mike’, Fuzz Type-Checker for Z, 26 Mart 2006 tarihinde kaynağından arşivlendi, erişim tarihi: 3 Mart 2017.
• Z/Eves — A proof checker for the Z notation (German site but all manuals in English)
• Z/EVES7 Ekim 2011 tarihinde Wayback Machine sitesinde arşivlendi. Documentation, papers, and manuals on Z/EVES
• ZETA open-source system for development software specifications in Z
• HOL-Z open-source proof environment for Z in Isabelle/HOL 5 Kasım 2015 tarihinde Wayback Machine sitesinde arşivlendi.
• CADiZ, Z gösteriminin kullanılmasına yardımcı olan bir dizi ücretsiz yazılım araçları
• ProofPower27 Aralık 2010 tarihinde Wayback Machine sitesinde arşivlendi., HOL'de ve Z notasyonunun belirtimi ve ispatı destekleyen açık kaynaklı araçlar paketi.
• z-vimes 1 Ağustos 2016 tarihinde Wayback Machine sitesinde arşivlendi. Z-Vimes: Z denetimi dili için tür denetleyicisi ve (sonuç olarak) teorem vericisi.
• ProB 25 Eylül 2015 tarihinde Wayback Machine sitesinde arşivlendi. Orijinal olarak B-Yöntemi için yazılmış ve Fuzz türü denetleyicisine uyan Z özelliklerini ("ProZ") de destekleyen bir animatör ve model denetleyicidir.