Perpustakaan Digital ITB

Meningkatnya kebutuhan manusia terhadap perangkat lunak menimbulkan kebutuhan yang sangat mendesak untuk program yang tidak memiliki kesalahan. Salah satu perangkat lunak yang dikembangkan untuk tujuan tersebut adalah Liquid Haskell untuk bahasa pemrograman Haskell. Sifat Liquid Haskell yang otomatis dan tidak memerlukan modifikasi kode dapat memudahkan proses verifikasi dengan sangat banyak sehingga memungkinkan verifikasi program yang lebih banyak dari sebelumnya. Namun kemudian timbul pertanyaan apakah Liquid Haskell benar-benar bisa memverifikasi semua program yang dituliskan dalam bahasa Haskell. Salah satu kasus yang sangat umum dijadikan contoh untuk mempelajari metode formal adalah kasus verifikasi struktur data Red-Black Tree atau Pohon MerahHitam (RBT). Pada 2010, Matthew Might membuat sebuah modifikasi terhadap struktur data RBT dengan tujuan untuk membuat sebuah algoritma penghapusan yang lebih elegan daripada algoritma yang sudah dituliskan sebelumnya. Struktur data ini merupakan struktur data yang sederhana dan memiliki spesifikasi yang sangat jelas dan mudah dituliskan sehingga algoritma ini bisa menjadi target yang tepat untuk membuktikan apakah Liquid Haskell bisa memverifikasi kode yang sudah ditulis oleh orang lain di dunia nyata. Hasil verifikasi dan analisis pada kode tersebut menunjukkan bahwa sebagian besar kode pada program berhasil diterima oleh verifikasi namun ada 3 bagian dari program yang digagalkan oleh verifikasi yaitu semua baris kode yang berhubungan dengan QuickCheck, properti BST untuk struktur pohon, serta baris terakhir pada fungsi balance. Oleh karena itu, dilakukan beberapa modifikasi kode sebagai contoh dari syntax yang dibutuhkan agak sebuah kode yang valid dapat diverifikasi dengan baik oleh Liquid Haskell.