Kita telah mengetahui bahwa sebuah algoritma yang baik adalah algoritma yang benar, efisien, dan mudah diimplementasikan. Pertanyaan berikutnya tentunya adalah, bagaimana kita mengetahui bahwa sebuah algoritma telah benar? Algoritma yang efisien itu seperti apa? Bagaimana kita mengukur kemudahan implementasi sebuah algoritma?
Bagian ini akan membahas mengenai pertanyaan pertama, yaitu bagaimana kita dapat mengetahui kebenaran sebuah algoritma. Tentunya efisiensi dan kemudahan implementasi sebuah algoritma menjadi tidak penting jika algoritma tersebut tidak dapat memberikan hasil yang benar.
Sebuah algoritma dikatakan telah benar jika algoritma tersebut dapat memberikan keluaran yang benar jika menerima masukan sesuai dengan definisi algoritma tersebut dan algoritma tersebut terbukti akan selalu dapat diterminasi (berakhir). Pembuktian kebenaran sebuah algoritma sendiri dapat dilakukan dengan beberapa cara, misalnya:
- Induksi Matematika
- Pembuktian kontradiktif
- Pembuktian kontrapositif, dan
- Metode Formal
Masing-masing alat pembuktian yang disebutkan memiliki kelebihan dan kekurangan masing-masing, serta kasus pengunaan yang berbeda-beda.
1. Induksi Matematika
Induksi matematika merupakan alat pembuktian matematis yang digunakan untuk membuktikan pernyataan atau proses yang melibatkan perhitungan bilangan asli yang berulang. Contoh dari rumus matematis yang dapat dibuktikan dengan menggunakan induksi matematika yaitu perhitungan deret aritmatika, deret geometris, ataupun sigma bilangan.
Pembuktian menggunakan induksi matematika dilakukan dengan dua langkah, yaitu:
-
Melakukan pembuktian kasus dasar (base case), yaitu membuktikan bahwa sebuah pernyataan (fungsi) matematika atau algoritma bernilai benar jika diaplikasikan pada bilangan pertama yang sah sesuai dengan spesifikasi fungsi atau algoritma tersebut.
-
Melakukan induksi, yaitu membuktikan bahwa kebenaran dari fungsi suatu algoritma jika kebenaran fungsi algoritma tersebut diketahui.
Dengan membuktikan kedua hal tersebut, kita dapat mengambil kesimpulan bahwa sebuah fungsi matematika atau algoritma bernilai benar untuk semua bilangan asli. Jika diimplementasikan dengan tepat, induksi matematika dapat juga digunakan untuk membuktikan kebenaran algoritma rekursif seperti penelusuran pohon (tree).
2.Pembuktian Kontradiktif
Pembuktian melalui kontradiksi adalah argumen logika yang dimulai dengan suatu asumsi, lalu dari asumsi tersebut diturunkan suatu hasil yang absurd, tidak masuk akal, atau kontradiktif, sehingga dapat diambil kesimpulan bahwa asumsi tadi adalah salah (dan ingkarannya benar).
Dalam disiplin matematika dan logika, pembuktian melalui kontradiktif merujuk secara khusus kepada argumen dimana sebuah kontradiktif dihasilkan dari suatu asumsi (sehingga membuktikan asumsi tadi salah). Argumen ini menggunakan hukum non-kontradiktif yaitu suatu pernyataan tidak mungkin benar dan salah sekaligus. Dalam disiplin logika formal, pembuktian melalui kontradiksi digunakan ketika sebuah kontradiksi (formal) dapat dihasilkan dari suatu premis, sehingga dapat disimpulkan bahwa premis tersebut salah. Jika kontradiksi tersebut dihasilkan dari beberapa (lebih dari satu) premis, kesimpulannya adalah satu atau lebih dari premis tersebut adalah salah. Dalam kasus terakhir, metode lain harus digunakan untuk membuktikan premis mana saja yang salah.
Suatu pernyataan matematis kadang-kadang dibuktikan dengan cara pembuktian melalui kontradiksi, dengan cara mengasumsikan ingkaran (negasi) dari pernyataan yang hendak dibuktikan, lalu dari asumsi ini diturunkan sebuah kontradiksi. Ketika kontradiksi dapat dicapai secara logika, asumsi tadi telah terbukti salah, sehingga pernyataan tersebut benar.
3. Pembuktian Kontrapositif
Logikanya, yang kontrapositif dari pernyataan kondisional dibentuk dengan meniadakan kedua istilah dan membalikkan arah inferensi. Secara eksplisit, yang kontrapositif dari pernyataan “jika A , maka B” adalah “jika tidak B, maka tidak A”. Sebuah pernyataan yang kontrapositif yang secara logis setara jika pernyataan itu benar , maka kontrapositifnya adalah benar dan sebaliknya.
Dalam matematika, bukti dengan kontraposisi adalah aturan inferensi yang digunakan dalam bukti. Aturan ini menyimpulkan pernyataan bersyarat dari kontrapositif-nya. Dengan kata lain, kesimpulan “jika A , maka B” diambil dari premis tunggal “ jika tidak B, maka tidak A”
4. Metode Formal
Metode formal adalah sebuah teknik dimana menggunakan basis logika matematika untuk membuat spesifikasi pada sistem komputer secara jelas dan terverifikasi. Kebenaran implementasi dari sebuah metode tersebut dijamin dengan kebenaran bukti matematis dari satu atau beberapa formula. Metode Formal menggunakan konsep matematika diskrit sebagai mekanisme representasi dengan demikian pembuktian logis dapat diterapkan pada masing-masing fungsi yang dimiliki sistem sehingga dapat diketahui bahwa spesifikasi dari tiap fungsi tersebut benar dan logis.
Sumber:
Metode and Correctness Algoritma
Pembuktian Kebenaran Algoritma