Celah Spesifikasi-Implementasi: Tempat Bug Bersembunyi

Ada klaim yang sesekali muncul di kalangan teori bahasa pemrograman: 'spesifikasi yang cukup detail tidak bisa dibedakan dari kode.' Implikasinya provokatif, yaitu garis antara mendeskripsikan apa yang seharusnya dilakukan program dan benar-benar melakukannya ternyata lebih tipis dari yang kita kira. Kalau spesifikasimu cukup presisi sampai tidak ada lagi ambiguitas, sebenarnya kamu sudah menulis programnya.

Ini bukan sekadar filsafat. Hal ini punya dampak praktis untuk cara kita membangun perangkat lunak, peran spesifikasi, dan alasan mengapa sebagian besar bug bukan kesalahan coding, melainkan celah spesifikasi. Memahami di mana spesifikasi berakhir dan implementasi dimulai akan mengubah cara kamu berpikir tentang testing, tipe, dan correctness.

Dari Mana Sebenarnya Sebagian Besar Bug Berasal

Tanyakan ke developer dari mana bug berasal dan biasanya mereka akan menjawab 'kode'. Tapi berbagai studi tentang cacat perangkat lunak menunjukkan hal yang berbeda: sebagian besar bug berasal dari celah antara maksud dan implementasi. Kode sudah melakukan persis apa yang diperintahkan developer. Masalahnya, perintah itu salah karena spesifikasi, baik formal maupun informal, ambigu, tidak lengkap, atau disalahpahami.

Contoh klasiknya: spesifikasi menyebut 'sistem harus menangani request secara konkuren'. Apa arti 'menangani'? Memprosesnya berurutan? Memprosesnya bersamaan? Mengantrekannya kalau terlalu banyak? Berapa 'terlalu banyak'? Apa yang terjadi pada request yang masuk saat antrean penuh? Pertanyaan-pertanyaan ini bukan detail implementasi, melainkan celah spesifikasi. Dan setiap pertanyaan yang belum terjawab adalah bug potensial, karena developer akan menjawabnya secara implisit lewat implementasi, dan jawabannya bisa jadi tidak sesuai dengan yang diharapkan pengguna atau developer lain.

Spektrum Presisi Spesifikasi

Spesifikasi ada dalam spektrum dari informal ke formal.

• Bahasa alami. 'Sistem login harus aman dan ramah pengguna.' Ini hampir tidak bisa disebut spesifikasi, lebih ke harapan. Setiap kata di situ ambigu. Apa yang dimaksud 'aman'? Apa yang dimaksud 'ramah pengguna'? Ini penilaian subjektif yang disamarkan sebagai requirement.
• Bahasa alami terstruktur. 'Ketika pengguna memasukkan password yang salah tiga kali dalam 10 menit, kunci akun selama 30 menit.' Lebih presisi, tapi tetap ambigu. Apakah 'password salah' termasuk submit kosong? Apakah tiga percobaan harus berurutan? Apakah jendela 10 menit itu bergulir atau tetap?
• Type signature. authenticate(username: string, password: string) -> Result<User, AuthError>. Ini mendefinisikan interface fungsi dengan presisi, tapi tidak berkata apa-apa soal perilakunya. Kamu tahu bentuk input dan output-nya, tapi bukan hubungan di antara keduanya.
• Spesifikasi berbasis properti. 'Untuk semua pasangan username-password yang valid di database, authenticate mengembalikan Ok(user) dengan user.username == username.' Ini membatasi perilaku lebih presisi dengan memakai quantifier logika.
• Spesifikasi formal. Model matematis lengkap tentang perilaku sistem, mencakup setiap state, setiap transisi, dan setiap invariant. Di level ini, spesifikasi dan implementasi hampir sama.

Semakin dekat kamu ke spesifikasi formal, semakin sedikit ruang untuk ambiguitas, dan semakin sedikit ruang untuk bug. Tapi setiap langkah juga butuh usaha lebih dan keahlian khusus. Pertanyaan praktisnya: seberapa jauh kamu perlu bergerak di sepanjang spektrum ini untuk sebuah proyek?

Tipe sebagai Spesifikasi Ringan

Sistem tipe adalah bentuk spesifikasi yang paling luas dipakai dalam pemrograman sehari-hari. Mereka memang tidak mendeskripsikan perilaku, tapi membatasinya. Fungsi yang mengembalikan Option<User> alih-alih User menyatakan bahwa user mungkin tidak ditemukan, dan compiler memaksa setiap pemanggil untuk menangani kemungkinan itu.

// The type signature IS a specification.
// This function takes a user ID and might not find a user.
// The compiler ensures every caller handles the None case.
fn find_user(id: UserId) -> Option<User> { ... }
// Compare with the stringly-typed version:
// fn find_user(id: &str) -> User  // What if ID is invalid?
//                                  // What if user not found?
//                                  // Does it panic? Return null?
//                                  // The type tells you nothing.
// Richer types encode more specification:
enum WithdrawError {
InsufficientFunds { available: Money, requested: Money },
AccountFrozen { reason: String, until: DateTime },
DailyLimitExceeded { limit: Money, spent: Money },
}
fn withdraw(account: &Account, amount: Money) -> Result<Transaction, WithdrawError>
// The error type specifies exactly what can go wrong and what
// information is available when it does. This is specification
// through the type system.

Bahasa seperti Rust, Haskell, dan TypeScript menunjukkan bagaimana sistem tipe yang ekspresif bisa mempersempit celah spesifikasi tanpa harus punya latar belakang metode formal. Algebraic data type, batasan generik, dan exhaustive pattern matching secara kolektif menspesifikasikan banyak perilaku program di level tipe, dan compiler memverifikasinya secara otomatis.

Insight utamanya: setiap anotasi tipe adalah spesifikasi yang dicek secara otomatis. Setiap perilaku yang bisa kamu encode di sistem tipe adalah satu kelas bug yang tidak akan pernah kamu alami.

Property-Based Testing: Mendefinisikan Perilaku

Unit test adalah spesifikasi berbasis contoh: 'dengan input spesifik ini, harapkan output spesifik itu.' Berguna, tapi pada dasarnya tidak lengkap, karena kamu hanya bisa menguji kasus yang terpikir olehmu. Property-based testing membalik pendekatan ini: kamu mendefinisikan properti yang harus berlaku untuk semua input, lalu framework testing menghasilkan input acak untuk mencari pelanggaran.

from hypothesis import given, strategies as st
# Unit test: one example
def test_sort_specific():
assert sort([3, 1, 2]) == [1, 2, 3]
# Property-based test: specifies what sort MEANS
@given(st.lists(st.integers()))
def test_sort_properties(lst):
result = sort(lst)
# Property 1: output has same length as input
assert len(result) == len(lst)
# Property 2: output is ordered
for i in range(len(result) - 1):
assert result[i] <= result[i + 1]
# Property 3: output contains the same elements
assert sorted(result) == sorted(lst)
# These three properties together SPECIFY sorting.
# Any function that satisfies all three IS a sort function.
# The property-based test IS the specification.

Tiga properti dalam test itu bukan sekadar menguji sorting, melainkan mendefinisikan sorting. Fungsi apa pun yang memenuhi ketiga properti itu secara definisi adalah sort yang benar. Ini ide 'spesifikasi sebagai kode' dalam bentuk paling praktis: tulis properti yang mendefinisikan perilaku benar, lalu biarkan framework testing memverifikasi bahwa implementasimu memenuhinya.

TLA+ dan Model Checking

Untuk sistem di mana bug itu mahal, seperti sistem terdistribusi, platform keuangan, dan infrastruktur kritis, alat spesifikasi formal seperti TLA+ memberikan jaminan yang lebih kuat. TLA+ (Temporal Logic of Actions) memungkinkanmu menspesifikasikan perilaku sistem sebagai state machine, lalu melakukan model checking: menjelajahi setiap kemungkinan eksekusi secara menyeluruh untuk memastikan invariant tetap terpenuhi.

Amazon sudah memakai TLA+ untuk memverifikasi algoritma di S3, DynamoDB, dan layanan kritis AWS lainnya. Mereka secara terbuka menceritakan bagaimana menemukan bug yang hampir mustahil ditemukan lewat testing, yaitu bug yang hanya muncul di interleaving tertentu dari operasi konkuren yang terjadi sekali dalam jutaan eksekusi.

Spesifikasi TLA+ untuk protokol konsensus seperti Raft biasanya hanya beberapa ratus baris. Di dalamnya didefinisikan setiap transisi state yang legal, setiap invariant (misalnya 'paling banyak satu leader per term'), dan setiap safety property. Model checker kemudian menjelajahi miliaran jalur eksekusi yang mungkin, memastikan tidak ada jalur yang melanggar invariant. Ini adalah spesifikasi yang benar-benar dekat dengan kode, cukup presisi sehingga kamu bisa menerjemahkannya secara mekanis menjadi implementasi.

Design by Contract

Design by Contract (DbC) dari Bertrand Meyer berada di posisi tengah yang praktis. Setiap fungsi mendefinisikan precondition (apa yang harus benar sebelum fungsi dipanggil), postcondition (apa yang dijamin fungsi saat selesai), dan invariant (apa yang harus selalu benar untuk objek tersebut). Kontrak ini dicek saat runtime selama development dan bisa dinonaktifkan di production demi performa.

def transfer(from_account, to_account, amount):
"""Transfer money between accounts.
Preconditions:
amount > 0
from_account.balance >= amount
from_account != to_account
Postconditions:
from_account.balance == old(from_account.balance) - amount
to_account.balance == old(to_account.balance) + amount
from_account.balance + to_account.balance ==
old(from_account.balance) + old(to_account.balance)
"""
# The postconditions above fully specify what this function does.
# The last postcondition (conservation) catches a class of bugs
# (money created or destroyed) that unit tests might miss.
assert amount > 0, "Transfer amount must be positive"
assert from_account.balance >= amount, "Insufficient funds"
assert from_account != to_account, "Cannot transfer to same account"
from_account.balance -= amount
to_account.balance += amount

Postcondition konservasi, yaitu total uang sebelum dan sesudah transfer harus sama, adalah jenis invariant yang sering luput dari unit test. Ini mendefinisikan properti fundamental sistem (uang tidak tercipta maupun hilang) yang harus dipenuhi implementasi yang benar.

Rekomendasi Praktis

Spesifikasi formal penuh memang tidak praktis untuk sebagian besar perangkat lunak. Tapi kamu bisa mempersempit celah spesifikasi secara signifikan dengan teknik yang muat di alur kerja development biasa.

1. Manfaatkan sistem tipe secara agresif. Encode batasan sebagai tipe kapan pun memungkinkan. Pilih NonEmptyList dibanding List ketika list tidak boleh kosong. Gunakan newtype wrapper untuk membedakan UserId dari OrderId meskipun keduanya string. Setiap batasan yang kamu encode di tipe adalah batasan yang dicek compiler secara gratis.
2. Tulis property-based test untuk logika inti. Identifikasi invariant yang harus dijaga sistemmu dan nyatakan sebagai property test. Beberapa properti yang dipilih dengan baik saja bisa menangkap bug yang terlewat dari ribuan test berbasis contoh.
3. Spesifikasikan batasan. Spesifikasi paling penting ada di batas sistem: kontrak API, skema database, dan format pesan. Gunakan OpenAPI, Protocol Buffers, atau JSON Schema agar bisa dicek secara mesin.
4. Gunakan TLA+ atau Alloy untuk sistem konkuren yang kritis. Kalau kamu merancang algoritma konsensus, distributed lock, atau sistem transaksi keuangan, biaya spesifikasi formal jauh lebih kecil dibanding biaya bug correctness yang halus di production.
5. Tulis spesifikasimu sebelum test. Kalau kamu tidak bisa menyatakan dengan tepat seperti apa perilaku yang benar, kamu tidak bisa memverifikasinya. Menghabiskan 30 menit untuk menulis spesifikasi yang jelas tentang apa yang seharusnya dilakukan sebuah fungsi (semua kasus, termasuk edge case) sering kali mengungkap masalah desain sebelum kamu menulis satu baris kode pun.

Klaim bahwa 'spesifikasi yang cukup detail adalah kode' sebenarnya kurang tepat. Lebih akurat dikatakan bahwa spesifikasi yang cukup detail menghilangkan ruang untuk bug. Celah antara spesifikasi dan implementasi adalah tempat ambiguitas hidup, dan ambiguitas adalah tempat bug berkembang biak. Setiap teknik yang mempersempit celah itu, seperti tipe, properti, kontrak, dan metode formal, membuat perangkat lunakmu lebih benar. Bukan karena mencegah kesalahan coding, tapi karena mencegah kesalahan spesifikasi yang biasanya menjadi sumber kesalahan coding.