Modul ini menutup jalur dengan pembuktian formal menggunakan SPARK. Empat topiknya membahas subset SPARK beserta batas-batasnya, alur kerja GNATprove beserta cara membaca hasil pemeriksaan, invarian loop untuk perulangan, serta kode ghost untuk properti khusus pembuktian. Materi modul menggunakan kontrak Pre dan Post dari modul sebelumnya dan menjadi dasar penerapan SPARK pada proyek nyata.
SPARK dan pembuktian
Subset SPARK, alur kerja GNATprove, invarian loop, dan kode ghost.
0/0 selesai
- Subset SPARK
Subset SPARK dari Ada: bagian yang dibuang dan alasan pembuangannya.
- Alur kerja GNATprove
Alur kerja GNATprove untuk menjalankan prover dan membaca hasil verifikasi.
- Invarian loop
Invarian loop agar loop dapat ditangani prover.
- Kode ghost
Kode ghost: konstruksi khusus pembuktian yang lenyap saat build.