Pelajari bagaimana karya Tony Hoare tentang logika Hoare, Quicksort, dan pemikiran keselamatan membentuk teknik praktis untuk menulis dan meninjau perangkat lunak yang benar.
Ketika orang mengatakan sebuah program “benar”, mereka seringkali maksudnya: “Saya menjalankannya beberapa kali dan keluarannya terlihat benar.” Itu sinyal berguna—tetapi bukan kebenaran. Secara sederhana, kebenaran berarti program memenuhi spesifikasinya: untuk setiap input yang diizinkan, ia menghasilkan hasil yang diminta dan menghormati aturan tentang perubahan status, waktu, dan penanganan kesalahan.
Masalahnya, “memenuhi spesifikasi” lebih sulit daripada kelihatannya.
Pertama, spesifikasi sering ambigu. Requirement produk mungkin mengatakan “urutkan daftar”, tetapi apakah itu berarti sorting stabil? Bagaimana dengan nilai duplikat, daftar kosong, atau item non-numerik? Jika spesifikasi tidak menyebutkan, orang berbeda akan mengasumsikan jawaban berbeda.
Kedua, kasus batas bukanlah langka—mereka hanya lebih jarang diuji. Nilai null, overflow, batas off-by-one, urutan pengguna yang tidak biasa, dan kegagalan eksternal yang tak terduga dapat mengubah “tampaknya bekerja” menjadi “gagal di produksi.”
Ketiga, requirements berubah. Sebuah program bisa benar relatif terhadap spesifikasi kemarin dan salah relatif terhadap spesifikasi hari ini.
Kontribusi besar Tony Hoare bukan klaim bahwa kita harus membuktikan semuanya sepanjang waktu. Kontribusinya adalah gagasan bahwa kita bisa lebih presisi tentang apa yang kode seharusnya lakukan—dan berpikir tentang itu dengan cara yang terdisiplin.
Di posting ini, kita akan mengikuti tiga benang yang saling terhubung:
Kebanyakan tim tidak akan menulis bukti formal lengkap. Tapi bahkan pemikiran “gaya bukti” parsial dapat membuat bug lebih mudah ditemukan, tinjauan lebih tajam, dan perilaku lebih jelas sebelum kode dikirim.
Tony Hoare adalah salah satu ilmuwan komputer langka yang karyanya tidak hanya tinggal di makalah atau ruang kelas. Ia bergerak antara akademia dan industri, dan peduli pada pertanyaan praktis yang masih dihadapi setiap tim: bagaimana kita tahu sebuah program melakukan apa yang kita kira—terutama ketika taruhannya tinggi?
Artikel ini fokus pada beberapa gagasan Hoare yang terus muncul di basis kode nyata:
{P} C {Q}.Anda tidak akan menemukan formalitas matematika yang mendalam di sini, dan kita tidak akan mencoba bukti Quicksort yang dapat diperiksa mesin sepenuhnya. Tujuannya adalah membuat konsep mudah didekati: struktur yang cukup untuk memperjelas penalaran Anda, tanpa mengubah tinjauan kode menjadi seminar pascasarjana.
Gagasan Hoare diterjemahkan ke keputusan biasa: asumsi apa yang diandalkan sebuah fungsi, apa yang dijaminkan kepada pemanggil, apa yang harus tetap benar di tengah loop, dan bagaimana mengenali perubahan yang “hampir benar” selama tinjauan. Bahkan saat Anda tidak menulis {P} C {Q} secara eksplisit, berpikir dalam bentuk itu memperbaiki API, tes, dan kualitas diskusi tentang kode rumit.
Pandangan Hoare lebih ketat daripada “lulus beberapa contoh”: kebenaran adalah tentang memenuhi janji yang disepakati, bukan tentang terlihat benar pada sampel kecil.
Bug sering terjadi ketika tim melewatkan langkah tengah: mereka lompat dari requirements langsung ke kode, membuat “janji” menjadi kabur.
Dua klaim berbeda sering dicampur:
Untuk sistem nyata, “tak pernah selesai” bisa sama berbahayanya dengan “selesai dengan jawaban yang salah.”
Pernyataan kebenaran tak pernah universal; mereka bergantung pada asumsi tentang:
Menjadi eksplisit tentang asumsi mengubah “bekerja di mesin saya” menjadi sesuatu yang dapat dipahami orang lain.
Pertimbangkan fungsi sortedCopy(xs).
Spesifikasi berguna bisa: “Mengembalikan daftar baru ys sehingga (1) ys terurut menaik, dan (2) ys berisi tepat elemen yang sama dengan xs (dengan jumlah yang sama), dan (3) xs tidak berubah.”
Sekarang “benar” berarti kode memenuhi tiga poin itu di bawah asumsi yang dinyatakan—bukan sekadar keluaran terlihat terurut pada pengujian cepat.
Logika Hoare adalah cara berbicara tentang kode dengan kejelasan yang sama seperti Anda berbicara tentang kontrak: jika Anda mulai dalam keadaan yang memenuhi asumsi tertentu, dan menjalankan potongan kode ini, Anda akan berakhir dalam keadaan yang memenuhi jaminan tertentu.
Notasi inti adalah tripel Hoare:
{precondition} program {postcondition}
Sebuah precondition menyatakan apa yang harus benar sebelum fragmen program dijalankan. Ini bukan tentang apa yang Anda harapkan; ini tentang apa yang kode butuh agar janjinya valid.
Contoh: misalkan sebuah fungsi mengembalikan rata-rata dua angka tanpa pemeriksaan overflow.
a + b muat dalam tipe integeravg = (a + b) / 2avg sama dengan rata-rata matematis a dan bJika precondition tidak terpenuhi (overflow mungkin terjadi), janji postcondition tidak lagi berlaku. Tripel memaksa Anda menyatakannya secara eksplisit.
Sebuah postcondition menyatakan apa yang akan benar setelah kode berjalan—dengan asumsi precondition terpenuhi. Postcondition yang baik konkret dan dapat diperiksa. Daripada mengatakan “hasil valid”, jelaskan apa arti “valid”: terurut, non-negatif, dalam batas, tak berubah kecuali pada bidang tertentu, dll.
Logika Hoare bisa diterapkan dari pernyataan kecil ke kode multi-langkah:
x = x + 1, fakta apa tentang x yang sekarang benar?Intinya bukan menaburkan kurung kurawal di mana-mana. Intinya membuat maksud dapat dibaca: asumsi jelas, hasil jelas, dan lebih sedikit percakapan “tampaknya bekerja” di tinjauan.
Sebuah invarian loop adalah pernyataan yang benar sebelum loop mulai, tetap benar setelah setiap iterasi, dan masih benar ketika loop selesai. Ide sederhana dengan keuntungan besar: ia menggantikan “tampaknya bekerja” dengan klaim yang bisa Anda periksa setiap langkah.
Tanpa invarian, sebuah tinjauan sering terdengar seperti: “Kita iterasi daftar dan perlahan memperbaiki hal.” Invarian memaksa presisi: apa yang sudah benar tepat saat ini, meskipun loop belum selesai? Setelah Anda bisa mengatakannya jelas, bug off-by-one dan kasus terlewat jadi lebih mudah terlihat, karena mereka muncul sebagai titik di mana invarian akan dilanggar.
Sebagian besar kode sehari-hari bisa memakai beberapa template andal.
1) Batas / keselamatan indeks
Menjaga indeks dalam rentang aman.
0 <= i <= nlow <= left <= right <= highJenis invarian ini bagus untuk mencegah akses di luar rentang dan membuat penalaran array menjadi konkret.
2) Item yang diproses vs belum diproses
Membagi data menjadi wilayah “selesai” dan “belum”.
a[0..i) telah diperiksa.”result memenuhi predikat filter.”Ini mengubah progres kabur menjadi kontrak jelas tentang apa arti “diproses”.
3) Prefix terurut (atau prefix terpartisi)
Umum pada pengurutan, penggabungan, dan partisi.
a[0..i) terurut.”a[0..i) <= pivot, dan semua item di a[j..n) >= pivot.”Bahkan jika seluruh array belum terurut, Anda sudah menetapkan bagian yang terikat.
Kebenaran bukan hanya tentang benar; loop juga harus selesai. Cara sederhana untuk berargumen adalah memberi nama sebuah ukuran (variant) yang mengecil setiap iterasi dan tidak bisa mengecil selamanya.
Contoh:
n - i mengecil 1 setiap kali.”Jika Anda tidak bisa menemukan ukuran yang mengecil, Anda mungkin menemukan risiko nyata: loop tak berujung pada beberapa input.
Quicksort punya janji sederhana: diberikan sebuah potongan (slice) atau segmen array, susun elemen-elemennya sehingga menjadi tidak menurun, tanpa kehilangan atau menambah nilai. Bentuk algoritma pada tingkat tinggi mudah diringkas:
Ini contoh pengajaran yang bagus karena cukup kecil untuk diingat, tetapi cukup kaya untuk menunjukkan di mana penalaran informal gagal. Quicksort yang “tampaknya bekerja” pada beberapa tes acak masih bisa salah pada input tertentu atau kondisi batas.
Beberapa isu yang menyebabkan kebanyakan bug:
Untuk berargumen kebenaran secara gaya Hoare, biasanya Anda pisahkan bukti menjadi dua bagian:
Pemecahan ini membuat penalaran lebih mudah dikelola: perbaiki partisi dulu, lalu bangun kebenaran pengurutan di atasnya.
Kecepatan Quicksort bergantung pada satu rutinitas yang tampak sepele: partisi. Jika partisi sedikit pun salah, Quicksort bisa salah urut, berputar selamanya, atau crash pada kasus batas.
Kita gunakan skema Hoare partition klasik (dua pointer bergerak ke dalam).
Input: sebuah potongan array A[lo..hi] dan nilai pivot yang dipilih (sering A[lo]).
Output: sebuah indeks p sedemikian sehingga:
A[lo..p] <= pivotA[p+1..hi] >= pivotPerhatikan apa yang tidak dijanjikan: pivot tidak mesti berakhir di posisi p, dan elemen yang sama dengan pivot bisa muncul di kedua sisi. Itu tidak apa-apa—Quicksort hanya butuh pemisahan yang benar.
Saat algoritma memajukan dua indeks—i dari kiri, j dari kanan—penalaran baik fokus pada apa yang sudah “terkunci”. Sekumpulan invarian praktis:
A[lo..i-1] adalah <= pivot (sisi kiri bersih)A[j+1..hi] adalah >= pivot (sisi kanan bersih)A[i..j] belum diklasifikasikan (masih harus diperiksa)Ketika kita menemukan A[i] >= pivot dan A[j] <= pivot, menukarnya mempertahankan invarian itu dan mengecilkan bagian yang belum diklasifikasikan.
i bergerak ke kanan; partisi harus tetap berhenti dan mengembalikan p yang masuk akal.j bergerak ke kiri; kekhawatiran terminasi sama.< vs <=), pointer bisa macet. Skema Hoare bergantung pada aturan konsisten agar progres berlangsung.Berbagai skema partisi ada (Lomuto, Hoare, partisi tiga-arah). Kuncinya adalah memilih satu, menyatakan kontraknya, dan meninjau kode terhadap kontrak itu secara konsisten.
Rekursi paling mudah dipercaya ketika Anda dapat menjawab dua pertanyaan dengan jelas: kapan berhenti? dan mengapa setiap langkah valid? Pemikiran ala Hoare membantu karena memaksa Anda menyatakan apa yang harus benar sebelum pemanggilan, dan apa yang akan benar setelahnya.
Sebuah fungsi rekursif butuh setidaknya satu kasus dasar di mana tidak ada pemanggilan rekursif lebih lanjut dan tetap memenuhi hasil yang dijanjikan.
Untuk pengurutan, kasus dasar tipikal adalah “array dengan panjang 0 atau 1 sudah terurut.” Di sini, “terurut” harus eksplisit: untuk relasi ≤, output terurut jika untuk setiap indeks i < j, kita punya a[i] ≤ a[j]. (Stabilitas—apakah elemen sama mempertahankan urutan awal—adalah properti terpisah; Quicksort biasanya tidak stabil kecuali didesain demikian.)
Setiap langkah rekursif harus memanggil dirinya pada input yang secara ketat lebih kecil. “Menyusut” ini adalah argumen terminasi: jika ukuran mengecil dan tidak bisa kurang dari 0, Anda tidak bisa rekursi selamanya.
Menyusut juga penting untuk keselamatan stack. Kode yang benar pun bisa crash jika kedalaman rekursi terlalu besar. Dalam Quicksort, partisi yang sangat tidak seimbang bisa menghasilkan kedalaman rekursi besar. Itu pengingat terminasi sekaligus pengingat praktis untuk mempertimbangkan kedalaman terburuk.
Kasus terburuk waktu Quicksort bisa memburuk menjadi O(n²) saat partisi sangat tidak seimbang, tetapi itu masalah kinerja—bukan kegagalan kebenaran. Tujuan penalaran di sini adalah: dengan asumsi langkah partisi mempertahankan elemen dan memisahkannya menurut pivot, pengurutan rekursif pada bagian yang lebih kecil berarti seluruh rentang memenuhi definisi terurut.
Testing dan penalaran gaya-bukti bertujuan pada tujuan yang sama—keyakinan—tetapi mencapai itu secara berbeda.
Tes sangat bagus untuk menangkap kesalahan konkret: off-by-one, kasus batas terlewat, regresi. Tapi suite tes hanya bisa mengambil sampel ruang input. Bahkan “100% coverage” tidak berarti “semua perilaku diperiksa”; biasanya itu berarti “semua baris dieksekusi.”
Penalaran gaya-bukti (khususnya logika Hoare) mulai dari spesifikasi dan bertanya: jika precondition ini terpenuhi, apakah kode selalu menegakkan postcondition? Ketika Anda melakukan itu dengan baik, Anda tidak hanya menemukan bug—Anda sering bisa mengeliminasi seluruh kategori bug (mis. “akses array tetap dalam batas” atau “loop tidak merusak properti partisi”).
Spesifikasi yang jelas adalah generator tes.
Jika postcondition Anda mengatakan “output terurut dan adalah permutasi dari input”, Anda otomatis mendapat ide tes:
<= pivot di kiri).Spesifikasi memberi tahu apa arti “benar”, dan tes memeriksa apakah kenyataan cocok dengannya.
Testing berbasis properti berada di antara bukti dan contoh. Alih-alih memilih beberapa kasus, Anda menyatakan properti dan membiarkan alat menghasilkan banyak input.
Untuk pengurutan, dua properti sederhana sangat berguna:
Properti ini pada dasarnya adalah postcondition yang ditulis sebagai pemeriksaan yang dapat dieksekusi.
Rutin ringan yang skalabel:
Jika Anda ingin menginstitusikan ini, buat “spes + catatan penalaran + tes” sebagai bagian dari template PR atau checklist tinjauan kode (lihat juga /blog/code-review-checklist).
Jika Anda menggunakan alur kerja pembuatan kode cepat dari antarmuka chat, disiplin yang sama berlaku—bahkan lebih penting. Di Koder.ai, misalnya, Anda bisa mulai di Planning Mode untuk menetapkan precondition/postcondition sebelum kode digenerasi, lalu iterasi dengan snapshot dan rollback sambil menambahkan tes berbasis properti. Alat mempercepat implementasi, tapi spes masih menjaga agar “cepat” tidak berubah jadi “rapuh.”
Kebenaran bukan hanya soal “program mengembalikan nilai yang benar.” Pemikiran keselamatan menanyakan: hasil apa yang tidak dapat diterima, dan bagaimana kita mencegahnya—bahkan ketika kode mendapat tekanan, disalahgunakan, atau sebagian gagal? Dalam praktik, keselamatan adalah kebenaran dengan sistem prioritas: beberapa kegagalan sekadar menyebalkan, yang lain bisa menyebabkan kerugian finansial, pelanggaran privasi, atau bahaya fisik.
Sebuah bug adalah cacat dalam kode atau desain. Sebuah bahaya (hazard) adalah situasi yang bisa mengarah pada hasil yang tidak dapat diterima. Satu bug bisa jadi tidak berbahaya di satu konteks dan berbahaya di konteks lain.
Contoh: off-by-one pada galeri foto mungkin salah memberi label gambar; kesalahan yang sama pada kalkulator dosis obat bisa mencelakai pasien. Pemikiran keselamatan memaksa Anda menghubungkan perilaku kode ke konsekuensi, bukan hanya ke “kepatuhan spes.”
Anda tidak perlu metode formal berat untuk mendapatkan manfaat keselamatan segera. Tim bisa mengadopsi praktik kecil dan bisa diulang:
Teknik ini berpadu alami dengan penalaran gaya Hoare: Anda buat precondition eksplisit (input yang diterima) dan pastikan postcondition mencakup properti keselamatan (apa yang tidak boleh terjadi).
Pengecekan berorientasi keselamatan punya biaya—waktu CPU, kompleksitas, atau penolakan palsu sesekali.
Pemikiran keselamatan lebih sedikit tentang membuktikan keindahan dan lebih banyak tentang mencegah mode kegagalan yang tidak bisa Anda tanggung.
Tinjauan kode adalah tempat di mana pemikiran kebenaran memberi hasil paling cepat, karena Anda bisa menemukan asumsi yang hilang jauh sebelum bug mencapai produksi. Gerakan inti Hoare—menyatakan apa yang harus benar sebelum dan apa yang akan benar setelah—terjemahannya mudah menjadi pertanyaan tinjauan.
Saat membaca perubahan, cobalah merangkai setiap fungsi kunci sebagai janji kecil:
Kebiasaan pemeriksa yang sederhana: jika Anda tidak bisa mengatakan pre/post dalam satu kalimat, kode kemungkinan perlu struktur yang lebih jelas.
Untuk fungsi berisiko atau sentral, tambahkan komentar kontrak kecil di atas tanda tangan. Buat konkret: input, output, efek samping, dan error.
def withdraw(account, amount):
"""Contract:
Pre: amount is an integer > 0; account is active.
Post (success): returns new_balance; account.balance decreased by amount.
Post (failure): raises InsufficientFunds; account.balance unchanged.
"""
...
Komentar ini bukan bukti formal, tetapi memberi pemeriksa sesuatu yang konkret untuk dicocokkan.
Jadilah ekstra eksplisit saat meninjau kode yang menangani:
Jika perubahan menyentuh hal-hal ini, tanyakan: “Apa preconditions-nya, dan di mana dipaksa?” dan “Jaminan apa yang kita berikan bahkan saat terjadi kegagalan?”
Penalaran formal tidak harus berarti mengubah seluruh basis kode menjadi makalah matematika. Tujuannya adalah menghabiskan kepastian ekstra di tempat yang memberi manfaat: lokasi di mana “terlihat baik di tes” tidak cukup.
Mereka cocok ketika Anda punya modul kecil dan kritis yang menjadi dasar banyak hal (auth, aturan pembayaran, izin, interlock keselamatan), atau algoritma rumit di mana kesalahan off-by-one bersembunyi lama (parser, scheduler, caching/eviction, primitif konkurensi, kode bergaya partisi/batas).
Aturan berguna: jika bug bisa menyebabkan bahaya nyata, kerugian besar, atau kerusakan data diam-diam, Anda ingin lebih dari sekadar tinjauan + tes biasa.
Anda bisa memilih dari “ringan” hingga “berat”, dan sering hasil terbaik datang dari kombinasi:
Tentukan kedalaman formalisasi dengan menimbang:
Dalam praktik, Anda juga bisa memperlakukan “formalitas” sebagai sesuatu yang ditambahkan bertahap: mulai dengan kontrak eksplisit dan invarian, lalu biarkan otomasi menjaga konsistensi. Untuk tim yang membangun cepat dengan Koder.ai—di mana menghasilkan front end React, backend Go, dan skema Postgres bisa terjadi cepat—snapshot/rollback dan ekspor kode memudahkan iterasi sambil tetap menegakkan kontrak lewat tes dan analisis statis di CI.
Gunakan ini sebagai gerbang singkat “haruskah kita memformalkan lebih?” saat perencanaan atau tinjauan:
Bacaan lanjutan: design-by-contract, testing berbasis properti, model checking untuk mesin status, analyzer statis untuk bahasa Anda, dan materi pengantar tentang proof assistant dan spesifikasi formal.
Kebenaran berarti program memenuhi spesifikasi yang disepakati: untuk setiap input yang diizinkan dan kondisi sistem yang relevan, program menghasilkan keluaran dan efek samping yang diminta (dan menangani kesalahan sesuai janji). “Tampaknya bekerja” biasanya berarti Anda hanya memeriksa beberapa contoh, bukan seluruh ruang input atau kondisi batas yang rumit.
Requirements adalah tujuan bisnis dalam bahasa biasa (mis. “urutkan daftar untuk ditampilkan”). Spesifikasi adalah janji yang tepat dan dapat diperiksa (mis. “mengembalikan daftar baru yang diurutkan menaik, memiliki multiset elemen yang sama, input tidak berubah”). Implementasi adalah kode yang Anda tulis. Bug sering terjadi ketika tim lompat langsung dari requirements ke implementasi tanpa menulis janji yang dapat diperiksa.
Kebenaran parsial: jika kode selesai (return), hasilnya benar. Kebenaran total: kode pasti selesai dan hasilnya benar — jadi terminasi termasuk dalam klaim.
Secara praktis, kebenaran total penting ketika “terjebak selamanya” adalah kegagalan yang terlihat pengguna, kebocoran sumber daya, atau risiko keselamatan.
Tripel Hoare {P} C {Q} dibaca seperti kontrak:
P (precondition): apa yang harus benar sebelum menjalankan CC: fragmen kodePrecondition adalah apa yang dibutuhkan kode (mis. “indeks berada dalam rentang”, “elemen bisa dibandingkan”, “lock dipegang”). Jika precondition bisa dilanggar oleh pemanggil, maka opsi Anda:
Kalau tidak, postcondition Anda menjadi sekadar harapan.
Invarian loop adalah pernyataan yang benar sebelum loop dimulai, tetap benar setelah setiap iterasi, dan masih benar saat loop selesai. Contoh template yang bisa dipakai:
0 <= i <= n)Jika Anda tidak bisa mengartikulasikan invarian, itu tanda loop melakukan terlalu banyak hal atau batasannya tidak jelas.
Biasanya Anda memberi nama sebuah ukuran (varian) yang berkurang setiap iterasi dan tidak bisa berkurang selamanya, mis.:
n - i menyusut satu per langkahJika Anda tidak menemukan ukuran yang berkurang, mungkin ada risiko non-terminasi (khususnya dengan duplikat atau pointer yang macet).
Dalam Quicksort, partisi adalah rutinitas kecil yang menjadi pondasi. Jika partisi sedikit pun salah, Anda bisa mendapatkan:
Karena itu, bantuannya menyatakan kontrak partisi secara eksplisit: apa yang harus benar di sisi kiri, di sisi kanan, dan bahwa elemen hanya diubah urutannya (permutasi).
Duplikat dan penanganan “sama dengan pivot” adalah titik kegagalan umum. Aturan praktis:
i/j yang macet)Jika duplikat sering terjadi, pertimbangkan partisi tiga-arah untuk mengurangi bug dan kedalaman rekursi.
Testing menemukan bug konkret; reasoning gaya-bukti dapat menyingkirkan kategori bug secara keseluruhan (keselamatan batas, pelestarian invarian, terminasi). Alur kerja hibrida yang praktis:
Untuk pengurutan, dua properti bernilai tinggi adalah:
Q (postcondition): apa yang akan benar setelah C selesai, dengan asumsi P terpenuhiAnda tidak perlu menulis notasi itu dalam kode—menggunakan strukturnya dalam tinjauan kode (“asumsi masuk, jaminan keluar”) adalah keuntungan praktis.