Kebenaran Program, Spesifikasi

Dari Wikipedia: Dalam ilmu komputer teoretis, kebenaran suatu algoritma dinyatakan ketika dikatakan bahwa algoritma tersebut benar sehubungan dengan spesifikasi.

Tetapi masalahnya adalah bahwa untuk mendapatkan spesifikasi "yang sesuai" bukanlah tugas yang sepele, dan tidak ada metode yang 100% benar (sejauh yang saya tahu) untuk mendapatkan yang benar, itu hanya perkiraan, jadi jika kita akan menganggap predikat sebagai spesifikasi hanya karena "terlihat" seperti "satu", mengapa tidak menganggap program itu benar hanya karena "terlihat" benar?

Pertama, Anda memang benar: Anda benar-benar peduli. Verifikasi formal mentransfer masalah kepercayaan dalam kebenaran program ke masalah kepercayaan dalam kebenaran spesifikasi, jadi itu bukan peluru perak.

Ada beberapa alasan mengapa proses ini masih bisa bermanfaat.

1. Spesifikasi seringkali lebih sederhana daripada kode itu sendiri. Misalnya, pertimbangkan masalah mengurutkan array bilangan bulat. Ada algoritma penyortiran yang cukup canggih yang melakukan hal-hal pintar untuk meningkatkan kinerja. Tetapi spesifikasinya cukup sederhana untuk dinyatakan: output harus dalam urutan yang meningkat, dan harus merupakan permutasi dari input. Dengan demikian, bisa dibilang lebih mudah untuk mendapatkan kepercayaan pada kebenaran spesifikasi daripada dalam kebenaran kode itu sendiri.

2. Tidak ada titik kegagalan tunggal. Misalkan Anda memiliki satu orang menuliskan spesifikasi, dan orang lain menulis kode sumber, dan kemudian secara resmi memverifikasi bahwa kode tersebut memenuhi spesifikasi. Maka setiap cacat terdeteksi harus hadir di kedua spec dan kode. Dalam beberapa kasus, untuk beberapa jenis cacat, ini terasa lebih kecil kemungkinannya: kecil kemungkinannya Anda akan mengabaikan kesalahan saat memeriksa spesifikasi dan mengabaikan kesalahan saat memeriksa kode sumber. Tidak semua, tetapi beberapa.

3. Spesifikasi parsial bisa jauh lebih sederhana daripada kode. Misalnya, pertimbangkan persyaratan bahwa program bebas dari kerentanan buffer overrun. Atau, persyaratan bahwa tidak ada kesalahan indeks array di luar batas. Ini adalah spesifikasi sederhana yang cukup jelas merupakan hal yang baik dan berguna untuk dapat dibuktikan. Sekarang Anda dapat mencoba menggunakan metode formal untuk membuktikan bahwa seluruh program memenuhi spesifikasi ini. Itu mungkin tugas yang cukup terlibat, tetapi jika Anda berhasil, Anda memperoleh kepercayaan diri yang meningkat pada program.

4. Spesifikasi mungkin berubah lebih jarang daripada kode. Tanpa metode formal, setiap kali kami memperbarui kode sumber, kami harus memeriksa secara manual bahwa pembaruan tidak akan menimbulkan bug atau kekurangan. Metode formal berpotensi mengurangi beban ini: misalkan spesifikasi tidak berubah, sehingga pembaruan perangkat lunak hanya melibatkan perubahan pada kode dan bukan perubahan pada spesifikasi. Kemudian untuk setiap pembaruan, Anda terbebas dari beban untuk memeriksa apakah spesifikasi masih benar (itu tidak berubah, jadi tidak ada risiko bug baru telah diperkenalkan dalam spesifikasi) dan dari beban untuk memeriksa apakah kode masih betul (verifikasi program memeriksa itu untuk Anda). Anda masih perlu memeriksa apakah spesifikasi asli sudah benar, tetapi Anda tidak perlu terus memeriksanya setiap kali pengembang melakukan patch / pembaruan / perubahan baru.

Akhirnya, ingat bahwa spesifikasi biasanya bersifat deklaratif dan tidak dapat selalu dieksekusi atau dikompilasi langsung ke kode. Sebagai contoh, pertimbangkan untuk menyortir lagi: spek mengatakan bahwa output meningkat dan merupakan permutasi dari input, tetapi tidak ada cara yang jelas untuk "mengeksekusi" spesifikasi ini secara langsung dan tidak ada cara yang jelas bagi kompiler untuk secara otomatis mengkompilasinya ke kode. Jadi, hanya mengambil spek sebagai benar dan menjalankannya sering bukan merupakan pilihan.

Meskipun demikian, intinya tetap sama: metode formal bukan obat mujarab. Mereka hanya memindahkan masalah kepercayaan (sangat sulit) dalam kebenaran kode ke masalah kepercayaan (hanya sulit) dalam kebenaran spec. Bug dalam spesifikasi adalah risiko nyata, umum, dan tidak dapat diabaikan. Memang, komunitas metode formal terkadang memisahkan masalah menjadi dua bagian: verifikasi adalah tentang memastikan kode memenuhi spesifikasi; validasi adalah tentang memastikan spesifikasi itu benar (memenuhi kebutuhan kami).

Anda mungkin juga menikmati verifikasi program formal dalam praktiknya dan mengapa kita tidak meneliti lebih lanjut tentang menyusun jaminan waktu? untuk perspektif lebih banyak dengan beberapa bantalan pada ini.

Jawaban DW itu bagus , tapi saya ingin memperluas pada satu titik. Spesifikasi bukan hanya referensi yang dengannya kode diverifikasi. Salah satu alasan untuk memiliki spesifikasi formal adalah untuk memvalidasinya dengan membuktikan beberapa properti mendasar. Tentu saja, spesifikasi tidak dapat sepenuhnya divalidasi - validasi akan serumit spesifikasi itu sendiri, sehingga itu akan menjadi proses tanpa akhir. Tetapi validasi memungkinkan kami mendapatkan jaminan yang lebih kuat pada beberapa properti penting.

Misalnya, Anda mendesain autopilot mobil. Ini adalah hal yang cukup rumit yang melibatkan banyak parameter. Sifat kebenaran autopilot meliputi hal-hal seperti "mobil tidak akan menabrak tembok" dan "mobil akan mengemudi ke tempat yang disuruh". Properti seperti "mobil tidak akan menabrak tembok" benar-benar sangat penting, jadi kami ingin membuktikannya. Karena sistem beroperasi di dunia fisik, Anda perlu menambahkan beberapa kendala fisik; properti sebenarnya dari sistem komputasi akan menjadi sesuatu seperti "di bawah asumsi ini mengenai ilmu material, dan asumsi ini mengenai persepsi hambatan oleh sensor mobil, mobil tidak akan menabrak dinding". Namun demikian, hasilnya adalah properti yang relatif sederhana yang jelas diinginkan.

Bisakah Anda membuktikan properti ini dari kode? Pada akhirnya, itulah yang terjadi, jika Anda mengikuti pendekatan yang sepenuhnya formal¹. Tetapi kodenya memiliki banyak bagian yang berbeda; rem, kamera, mesin, dll. semuanya dikendalikan secara otonom. Properti kebenaran dari rem akan menjadi sesuatu seperti "jika sinyal 'terapkan rem' diaktifkan maka rem diterapkan". Properti kebenaran mesin adalah "jika sinyal kopling mati maka mesin tidak menggerakkan roda". Dibutuhkan pandangan tingkat tinggi untuk menggabungkan semuanya. Spesifikasi menciptakan lapisan perantara di mana komponen yang berbeda dari sistem dapat diartikulasikan bersama.

Bahkan, sistem yang rumit seperti autopilot mobil akan memiliki beberapa tingkat spesifikasi dengan jumlah penyempurnaan yang berbeda-beda. Pendekatan penyempurnaan sering digunakan dalam desain: mulai dengan beberapa properti tingkat tinggi seperti "mobil tidak akan menabrak dinding", kemudian mencari tahu bahwa ini memerlukan sensor dan rem dan bekerja beberapa persyaratan dasar untuk sensor, rem dan perangkat lunak perintis, kemudian menyempurnakan kembali persyaratan dasar tersebut menjadi desain komponen (untuk sensor, saya akan memerlukan radar, DSP, perpustakaan pemrosesan gambar, ...), dll. Dalam proses pengembangan formal, setiap tingkat spesifikasi terbukti memenuhi persyaratan yang ditetapkan oleh tingkat di atasnya, mulai dari properti tingkat tertinggi hingga kode.

Tidak mungkin untuk memastikan bahwa spesifikasinya benar. Misalnya, jika Anda salah memahami fisika, rem mungkin tidak efektif meskipun matematika yang menghubungkan kode rem dengan persyaratan formal benar. Tidak ada gunanya membuktikan bahwa jeda itu efektif dengan beban 500kg jika Anda benar-benar memiliki 5000kg. Tetapi lebih mudah untuk melihat bahwa 500kg salah daripada melihat di dalam kode rem bahwa mereka tidak akan cukup baik untuk parameter fisik mobil.

¹ _{Kebalikan dari pendekatan formal sepenuhnya adalah "Saya kira ini berhasil, tetapi saya tidak bisa memastikan". Ketika Anda mempertaruhkan hidup Anda untuk itu, itu tidak tampak hebat.}