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 olarakbilgisayar programıve bilgisayar tabanlı sistemlerin belirtilmesi hedeflenmektedir.
Tarihi
[değiştir|kaynağı değiştir]1974'teJean-Raymond Abrial"Veri Semantiği" ni yayınladı.[1]Daha sonra 1980'lerin sonuna kadarGrenoble Ü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 veBertrand 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ğiProgramlama Araştırma Grubu'ndaOxford Üniversitesi'nde geliştirildi.
Araçlar
[değiştir|kaynağı değiştir]- Community Z Tools (CZT)(project), Source forge, 1 Temmuz 2004 tarihindekaynağındanarşivlendi,erişim tarihi:3 Mart2017.
- Z Word tools(project), Source forge, 24 Mart 2017 tarihinde kaynağındanarşivlendi,erişim tarihi:3 Mart2017for developing and checking Z specifications inMicrosoft Word.
- Spivey, Michael ‘Mike’,Fuzz Type-Checker for Z,26 Mart 2006 tarihindekaynağındanarşivlendi,erişim tarihi:3 Mart2017.
- Z/Eves — A proof checker for the Z notation(German site but all manuals in English)
- Z/EVES7 Ekim 2011 tarihindeWayback Machinesitesindearş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/HOL5 Kasım 2015 tarihindeWayback Machinesitesindearşivlendi.
- CADiZ,Z gösteriminin kullanılmasına yardımcı olan bir dizi ücretsiz yazılım araçları
- ProofPower27 Aralık 2010 tarihindeWayback Machinesitesindearşivlendi., HOL'de ve Z notasyonunun belirtimi ve ispatı destekleyen açık kaynaklı araçlar paketi.
- z-vimes1 Ağustos 2016 tarihindeWayback Machinesitesindearşivlendi.Z-Vimes: Z denetimi dili için tür denetleyicisi ve (sonuç olarak) teorem vericisi.
- ProB25 Eylül 2015 tarihindeWayback Machinesitesindearş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.
Kaynakça
[değiştir|kaynağı değiştir]- ^Abrial, Jean-Raymond(1974), "Data Semantics", Klimbie, J.W.; Koffeman, K.L. (Ed.),Proceedings of theIFIPWorking Conference on Data Base Management,North-Holland,ss. 1-59.
- ^Meyer, Bertrand;Baudoin, Claude (1980),Méthodes de programmation(Fransızca),Eyrolles.
- ^Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980), "A Specification Language", Macnaghten, AM; McKeag, RM (Ed.),On the Construction of Programs,Cambridge University Press,ISBN0-521-23090-X(describes early version of the language).
Daha fazla bilgi
[değiştir|kaynağı değiştir]- Spivey, John Michael(1992).The Z Notation: A reference manual.International Series in Computer Science. Prentice Hall. 9 Ekim 2008 tarihindekaynağındanarşivlendi.Erişim tarihi:3 Mart2017.
- Davies, Jim;Woodcock, Jim(1996).Using Z: Specification, Refinement and Proof.International Series in Computer Science. Prentice Hall.ISBN0-13-948472-8.27 Haziran 2009 tarihindekaynağındanarşivlendi.Erişim tarihi:3 Mart2017.
- Bowen, Jonathan(1996).Formal Specification and Documentation using Z: A Case Study Approach.International Thomson Computer Press.ISBN1-85032-230-9.4 Mart 2017 tarihinde kaynağındanarşivlendi.Erişim tarihi:3 Mart2017.
- Jacky, Jonathan (1997).The Way of Z: Practical Programming with Formal Methods.Cambridge University Press.ISBN0-521-55976-6.3 Ocak 2017 tarihinde kaynağındanarşivlendi.Erişim tarihi:3 Mart2017.
Dış bağlantılar
[değiştir|kaynağı değiştir]- Toyn, Ian,Z Specification proposals,UK:York, 22 Haziran 2012 tarihindekaynağındanarşivlendi,erişim tarihi:3 Mart2017.
- WSDL 2.0,W3C, 4 Mart 2017 tarihinde kaynağındanarşivlendi,erişim tarihi:3 Mart2017,a specification containing Z notation assertions and explanation