Notasi Z dalam Spesifikasi Formal Program Aplikasi Smart Card

Abstract

Notasi Z telah diafui kehandalannya sebagai alat bantu pembuatan dolatmen spesifikasi F:ot dalam proses pengembangan suatu program aplikasi. Tulisan ini memberikan uritian *kas pembuatan dolcumen spesifikasi formal dengan notasi Z dalam proses pengembangan Ircgram aplikasi smart card untuk keperluan perpustakaan, beserta analisanya. Dimulai dengan gifkasi dalam bahasa alamiah (bahasa Indonesia), yang kemudian dijabarkan secera forntal fun notasi Z yang berbasis pada model matematika. Selanjutnya, dilakukan pengujian terhadap del tersebut dengan menggunakan fuzz2000, yaitu suatu program aplikasi yang dapat menguji nryfrat ahtrasi, konsistensi dan kelengkapan dari model matematika dalam notasi Z. Didiskusikan pda beberapa faktor yang menjadi kendala saat digunakannya bentuk spesifikasi formal dalant pros es p en gem b an g an p r o gr am ap likns i t er s e but.