Di Software Engineering Stack Exchange, saya melihat pertanyaan ini : "Apa yang menghentikan adopsi metode formal yang meluas?" Pertanyaan itu ditutup karena bias, dan sebagian besar jawabannya adalah komentar seperti "Terlalu mahal !!!" atau "Situs bukan pesawat !!!" Di satu sisi, ini benar, tetapi itu tidak menjelaskan banyak hal. Saya menulis artikel ini untuk memberikan gambaran sejarah yang lebih luas tentang metode formal (FM), mengapa mereka tidak benar-benar digunakan, dan apa yang kita lakukan untuk memperbaiki situasi.

Sebelum Anda mulai, Anda perlu merumuskan beberapa kondisi. Faktanya, tidak ada banyak metode formal: hanya beberapa kelompok kecil . Ini berarti bahwa kelompok yang berbeda menggunakan istilah secara berbeda. Secara umum, ada dua kelompok metode formal: spesifikasi formal mempelajari penulisan spesifikasi yang spesifik dan tidak ambigu, dan verifikasi formal mempelajari metode pembuktian. Ini termasuk kode dan sistem abstrak. Kami tidak hanya menggunakan istilah yang berbeda untuk kode dan sistem, kami sering menggunakan alat yang berbeda untuk memverifikasinya. Untuk membuat segalanya lebih membingungkan, jika seseorang mengatakan bahwa dia membuat spesifikasi formal, ini biasanya berarti verifikasi desain. Dan jika seseorang mengatakan bahwa dia melakukan verifikasi formal, ini biasanya mengacu pada verifikasi kode.

Untuk kejelasan, kami akan membagi verifikasi menjadi verifikasi kode (CV) dan verifikasi desain (DV) dan dengan cara yang sama membagi spesifikasi menjadi CS dan DS. Istilah seperti itu tidak umum digunakan dalam komunitas FM yang luas. Mari kita mulai dengan CS dan CV, lalu beralih ke DS dan DV.

Selain itu, verifikasi parsial dimungkinkan, di mana hanya sebagian dari spesifikasi yang diperiksa, atau verifikasi lengkap . Ini mungkin perbedaan antara bukti dugaan “sistem tidak pernah crash dan tidak menerima kata sandi yang salah” atau “sistem tidak pernah crash dan mengunci akun jika Anda memasukkan kata sandi yang salah tiga kali”. Pada dasarnya, kami akan menganggap bahwa kami sedang melakukan pemeriksaan penuh.

Anda juga harus mengklarifikasi jenis perangkat lunak yang kami formalkan. Kebanyakan orang secara implisit mengidentifikasi program yang sangat andal seperti perangkat medis dan pesawat terbang. Orang berasumsi bahwa metode formal banyak digunakan untuk mereka, tetapi mereka tidak diperlukan untuk yang lain. Ini terlalu optimis : sebagian besar perangkat lunak yang sangat andal tidak menggunakan metode formal. Sebaliknya, kami akan fokus pada perangkat lunak "biasa".

Akhirnya, penafian: Saya bukan sejarawan profesional, dan meskipun saya mencoba untuk memverifikasi informasi dengan hati-hati, mungkin ada kesalahan dalam artikel. Selain itu, saya mengkhususkan diri dalam spesifikasi formal (DS dan DV), sehingga ada lebih banyak kemungkinan kesalahan di mana saya berbicara tentang verifikasi kode. Jika Anda melihat, menulis kepada saya, saya akan memperbaikinya (dan satu hal lagi: saya mendapatkan uang dari seminar di TLA + dan Alloy, oleh karena itu saya sangat bias terhadap bahasa-bahasa ini; Saya mencoba untuk seobjektif mungkin, tetapi Anda mengerti: bias bias).

Pemrograman formal

Mendapatkan spesifikasi

Sebelum membuktikan kebenaran kode, Anda perlu mendapatkan standar kebenaran. Ini berarti beberapa spesifikasi tentang apa yang harus dilakukan kode. Kita harus tahu pasti bahwa hasilnya sesuai dengan spesifikasi. Tidaklah cukup untuk mengatakan bahwa daftar itu "diurutkan": kami tidak tahu apa yang kami sortir, kriteria apa yang kami gunakan dan bahkan apa yang kami maksud dengan "sortasi". Sebagai gantinya, kita dapat mengatakan: "Daftar bilangan bulat l diurutkan dalam urutan naik untuk dua indeks i dan j, jika i < j , maka l[i] <= l[j] ."

Spesifikasi kode dibagi menjadi tiga jenis utama:

Yang pertama adalah menulis pernyataan bebas kode. Kami menulis fungsi penyortiran kami, dan dalam file terpisah kami menulis teorema "ini mengembalikan daftar diurutkan". Ini adalah bentuk spesifikasi tertua, tetapi Isabelle dan ACL2 masih berfungsi seperti ini (ML diciptakan khusus untuk membantu menulis spesifikasi semacam itu).
Yang kedua memperkenalkan spesifikasi ke dalam kode dalam bentuk prakondisi dan postkondisi, pernyataan dan invarian. Anda dapat menambahkan postcondition ke fungsi yang "nilai kembali adalah daftar yang diurutkan." Spesifikasi berbasis klaim pada awalnya diresmikan sebagai logika Hoar . Mereka pertama kali muncul dalam bahasa pemrograman Euclid pada awal 1970-an (tidak jelas siapa yang mulai menggunakannya: Euclid atau SPV , tetapi sejauh yang saya tahu, Euclid diperkenalkan kepada publik sebelumnya). Gaya ini juga disebut pemrograman kontrak - bentuk verifikasi paling populer di industri modern (di sini, kontrak digunakan sebagai spesifikasi kode).
Akhirnya, ada sistem tipe. Oleh Curry - korespondensi Howard, setiap teorema atau bukti matematika dapat dikodekan sebagai tipe dependen. Kami akan menentukan jenis daftar yang diurutkan dan mendeklarasikan jenis [Int] -> Sorted [Int] untuk fungsi tersebut.

Pada Let's Prove Leftpad, Anda dapat melihat tampilannya. HOL4 dan Isabelle adalah contoh yang baik dari spesifikasi "theorem independen", SPARK dan Dafny adalah spesifikasi dari "pernyataan bersarang", dan Coq dan Agda adalah "tipe dependen".

Jika Anda perhatikan lebih dekat, ketiga bentuk spesifikasi kode ini dibandingkan dengan tiga area utama validasi otomatis: tes, kontrak, dan tipe. Ini bukan kebetulan. Kebenaran adalah beragam, dan verifikasi formal adalah salah satu yang ekstrem. Karena ketelitian (dan upaya) verifikasi menurun, kami mendapatkan pemeriksaan yang lebih sederhana dan lebih sempit, apakah itu membatasi ruang keadaan yang sedang dipelajari, menggunakan tipe yang lebih lemah, atau pengecekan paksa saat runtime. Kemudian segala cara spesifikasi lengkap berubah menjadi sarana spesifikasi parsial, dan sebaliknya: banyak yang menganggap Cleanroom teknik verifikasi formal, di mana tinjauan kode jauh melampaui kemampuan manusia.

Spesifikasi mana yang benar?

Verifikasi memverifikasi bahwa kode tersebut sesuai dengan spesifikasi. Muncul pertanyaan: bagaimana kita tahu bahwa kita memiliki spesifikasi yang tepat? Menemukan spesifikasi yang tepat adalah salah satu masalah terbesar dalam metode formal. Ini juga salah satu keberatan utama mereka. Tetapi skeptis di sini tidak berarti persis apa yang ada dalam pikiran formal.

Ketika orang luar bertanya, "Bagaimana Anda mendapatkan spesifikasi yang tepat?" Mereka biasanya berpikir tentang validasi , yaitu spesifikasi yang tidak memenuhi persyaratan klien. Jika Anda secara resmi membuktikan bahwa kode Anda mengurutkan daftar, dan klien benar-benar menginginkan Uber untuk sup (tm), Anda hanya menghabiskan banyak waktu. Seperti, hanya iterasi cepat dan putaran umpan balik pendek yang dapat mengkonfirmasi kebutuhan Anda.

Benar bahwa verifikasi kode tidak memvalidasinya. Namun ada dua masalah dengan argumen ini. Yang pertama adalah bahwa tahap penerapan metode formal hanya ditunda, tetapi tidak sepenuhnya hilang. Setelah semua iterasi cepat ini, Anda mungkin sudah memiliki gagasan tentang apa yang diinginkan klien. Dan kemudian Anda mulai verifikasi kode. Kedua, meskipun kita tidak tahu persis apa yang diinginkan klien, kita dapat mengasumsikan apa yang jelas tidak diinginkannya. Contohnya, hingga crash software secara tidak sengaja. Mereka tidak membutuhkan lubang keamanan. Semua orang setuju dengan ini: pada akhirnya, tidak ada yang mengatakan bahwa Anda perlu melewati tes unit selama iterasi. Jadi setidaknya pastikan bahwa sistem kontrol versi Anda tidak menghapus data pengguna acak (catatan: jangan berpikir bahwa saya sakit hati atau semacamnya).

Masalah dengan menemukan spesifikasi yang tepat lebih mendasar: kita sering tidak tahu harus menulis apa di sana . Kami memikirkan persyaratan kami dalam istilah manusia, bukan matematika. Jika saya mengatakan: "Program ini harus membedakan pohon dari burung," lalu tentang apa? Saya bisa menjelaskannya kepada seseorang dengan menunjukkan banyak gambar pohon dan burung, tetapi ini hanyalah contoh nyata, bukan deskripsi dari ide tersebut . Bahkan, untuk menerjemahkan ini ke dalam spesifikasi formal, perlu untuk memformalkan konsep manusia, dan ini adalah masalah serius.

Jangan salah sangka. Spesifikasi yang relevan dapat didefinisikan di sini, dan para ahli melakukan ini setiap saat. Tetapi menulis spesifikasi yang sesuai adalah keterampilan yang perlu dikembangkan, serta keterampilan pemrograman. Inilah sebabnya mengapa banyak keberhasilan verifikasi kode baru-baru ini dijelaskan oleh pemetaan yang jelas tentang apa yang kita inginkan menjadi apa yang dapat kita ungkapkan. Sebagai contoh, CompCert adalah kompiler C yang terverifikasi secara formal. Spesifikasinya adalah: "Hindari kesalahan kompilasi".

Tetapi semua ini tidak ada hubungannya dengan verifikasi. Ketika Anda memiliki spesifikasi, Anda masih perlu membuktikan bahwa kode tersebut cocok dengan itu.

Bukti spesifikasi

Alat verifikasi kode yang pertama adalah metode "pikirkan tentang mengapa ini benar" gaya Dijkstra, yang terutama untuk ALGOL. Misalnya, saya dapat "membuktikan" kebenaran penyortiran dengan metode penyisipan sebagai berikut:

Opsi dasar : jika Anda menambahkan satu elemen ke daftar kosong, itu akan menjadi satu-satunya elemen, sehingga akan diurutkan.
Jika kita memiliki daftar yang diurutkan dengan elemen k dan menambahkan satu elemen, maka kita memasukkan elemen itu setelah semua angka yang lebih kecil dan sebelum semua angka yang lebih besar. Ini artinya daftarnya masih disortir.
Dengan induksi, penyortiran penyisipan akan mengurutkan seluruh daftar.

Jelas, pada kenyataannya, buktinya akan terlihat lebih keras, tetapi ini adalah ide umum. Dijkstra dan yang lainnya menggunakan gaya ini untuk membuktikan kebenaran dari banyak algoritma, termasuk banyak dasar-dasar konkurensi. Ini juga gaya yang terkait dengan kata - kata Knuth : “Waspadalah terhadap kesalahan dalam kode ini; Saya hanya membuktikan bahwa itu benar, tetapi tidak memulainya. " Anda dapat dengan mudah merusak bukti matematika sehingga tidak ada yang akan memperhatikan. Menurut beberapa perkiraan , sekitar 20% dari bukti matematika yang dipublikasikan mengandung kesalahan. Peter Guttmann memiliki esai yang sangat baik tentang bukti kesehatan program konyol, di mana banyak kode "diuji" segera jatuh jika Anda menjalankannya.

Pada saat yang sama, kami mempelajari cara untuk membuktikan teorema matematika secara otomatis. Program pertama untuk membuktikan teorema diterbitkan pada tahun 1967 . Pada awal 1970-an, program semacam itu mulai digunakan untuk menguji kode Pascal, dan pada pertengahan dekade muncul bahasa formal khusus. Programmer merumuskan beberapa properti kode, dan kemudian membuat bukti yang dapat diverifikasi bahwa kode memiliki properti ini. Program pertama untuk membuktikan teorema hanya membantu orang memverifikasi bukti, sementara alat yang lebih canggih dapat secara independen membuktikan bagian dari teorema.

Yang mengarah pada masalah berikut.

Bukti sulit didapat

Bukti sulit, dan itu adalah pekerjaan yang sangat buruk. Sulit untuk berhenti pemrograman dan pergi ke sirkus. Anehnya, bukti formal kode sering lebih ketat daripada bukti yang ditulis oleh sebagian besar ahli matematika! Matematika adalah kegiatan yang sangat kreatif, di mana jawaban atas teorema hanya valid jika Anda menunjukkannya. Kreativitas berjalan buruk dengan formalisme dan komputer.

Ambil contoh penyortiran penyisipan yang sama di mana kami menerapkan induksi. Matematikawan mana pun akan segera memahami apa itu induksi, cara kerjanya secara umum, dan cara kerjanya dalam kasus ini. Tetapi dalam program untuk membuktikan teorema semuanya perlu diformalkan secara ketat. Hal yang sama berlaku dengan bukti oleh kontradiksi, bukti melalui kontra-posisi, dll. Selain itu, semua asumsi harus diformalkan, bahkan mereka yang sebagian besar matematikawan tidak peduli dengan bukti. Misalnya, a + (b + c) = (a + b) + c . Program untuk memeriksa teorema a priori tidak tahu bahwa ini benar. Anda harus membuktikannya (sulit), atau menyatakannya sebagai kebenaran sesuai dengan hukum tambahan asosiatif (berbahaya), atau membeli perpustakaan teorema dari seseorang yang sudah dapat membuktikannya (mahal). Program pembuktian teorema awal berkompetisi dalam sejumlah taktik pembuktian bawaan dan perpustakaan teorema terkait. Salah satu program SPADE luas pertama disajikan perpustakaan aritmatika lengkap sebagai keuntungan utama.

Selanjutnya, Anda perlu mendapatkan buktinya sendiri. Anda dapat mempercayakan ini ke program atau menulisnya sendiri. Biasanya definisi otomatis bukti tidak dapat ditentukan. Untuk kasus yang sangat sempit, seperti logika proposisional atau tipe yang memeriksa HM, ini "hanya" NP-lengkap. Faktanya, kami sendiri yang menulis sebagian besar bukti, dan komputer memeriksa kebenarannya. Ini berarti bahwa Anda perlu tahu dengan baik:

matematika
ilmu komputer;
area tempat Anda bekerja: kompiler, perangkat keras, dll.
nuansa program dan spesialisasi Anda;
nuansa program untuk membuktikan teorema yang Anda gunakan, yang dengan sendirinya merupakan spesialisasi khusus.

Lebih buruk lagi, tongkat khusus komputer dimasukkan ke roda. Ingat, saya katakan itu berbahaya untuk mengasumsikan hukum asosiatif tambahan? Beberapa bahasa tidak mematuhinya. Misalnya, dalam C ++ INT_MAX. ((-1) + INT_MAX) + 1 INT_MAX. ((-1) + INT_MAX) + 1 adalah INT_MAX. -1 + (INT_MAX + 1) INT_MAX. -1 + (INT_MAX + 1) , yang tidak dapat dideteksi. Dengan asumsi penambahan asosiatif dalam C ++, bukti Anda akan salah, dan kode akan rusak. Anda harus menghindari pernyataan ini atau membuktikan bahwa luapan tidak akan pernah terjadi untuk fragmen khusus Anda.

Anda dapat mengatakan bahwa penambahan yang tidak terbatas adalah kesalahan, tetapi Anda perlu menggunakan bahasa dengan bilangan bulat yang tidak terkait. Tetapi sebagian besar bahasa memiliki fitur spesifik yang mengganggu bukti. Ambil kode berikut:

 a = true; b = false; f(a); assert a;

Apakah ini selalu terjadi? Bukan fakta. Mungkin f akan berubah a . Mungkin itu akan mengubah aliran paralel. Mungkin b diberi alias, jadi mengubahnya juga akan mengubah (catatan: alias membuatnya sangat sulit untuk menulis bukti bahwa John C. Reynolds harus membuat logika pemisahan yang sama sekali baru untuk menangani masalah ini). Jika sesuatu seperti ini dimungkinkan dalam bahasa Anda, maka Anda harus dengan jelas membuktikan bahwa ini tidak terjadi di sini. Kode bersih akan membantu di sini, dalam kasus lain, itu dapat menghancurkan buktinya, karena itu memaksa Anda untuk menggunakan rekursi dan fungsi dari urutan yang lebih tinggi. Omong-omong, keduanya adalah dasar untuk menulis program fungsional yang baik. Apa yang baik untuk pemrograman tidak baik untuk pembuktian! (Catatan: dalam kuliah ini, Edmund Clark mendaftarkan beberapa properti yang sulit untuk diverifikasi: "floating point, string, tipe yang ditentukan pengguna, prosedur, konkurensi, templat universal, penyimpanan, perpustakaan ...").

Penguji formal memiliki dilema: semakin ekspresif bahasa, semakin sulit untuk membuktikan sesuatu. Tetapi semakin kurang ekspresif bahasa, semakin sulit untuk menulisnya. Bahasa formal pertama yang bekerja adalah himpunan bagian yang sangat terbatas dari bahasa yang lebih ekspresif: ACL2 adalah bagian dari Lisp, Euclid adalah bagian dari Pascal, dll. Dan tidak ada apa pun yang telah kita bahas sejauh ini yang benar-benar membuktikan program nyata, ini hanya upaya untuk mendekati untuk menulis bukti.

Buktinya sulit. Tetapi semakin mudah. Para peneliti di bidang ini menambahkan heuristik baru, perpustakaan teorema, komponen pra-diuji, dll. Kemajuan teknis juga membantu: semakin cepat komputer, semakin cepat pencarian.

Revolusi SMT

Salah satu inovasi pada pertengahan 2000-an adalah dimasukkannya SMT solver dalam program untuk membuktikan teorema. Secara umum, seorang pemecah SMT dapat mengubah (beberapa) teorema matematika menjadi masalah kepatuhan kendala. Ini mengubah tugas kreatif menjadi tugas komputasi. Anda mungkin masih perlu mengisinya dengan masalah menengah (lemmas) sebagai langkah dalam teorema, tetapi ini lebih baik daripada membuktikan semuanya sendiri. Pemecah SMT pertama muncul sekitar tahun 2004, pertama sebagai proyek akademik. Beberapa tahun kemudian, Microsoft Research merilis Z3, sebuah solver SMT yang siap pakai. Keuntungan besar Z3 adalah menjadi lebih nyaman untuk digunakan daripada SMT lain, yang, terus terang, hampir tidak mengatakan apa-apa. Microsoft Research menggunakannya secara internal untuk membantu membuktikan sifat-sifat kernel Windows, sehingga mereka tidak terbatas pada minimal UX.

TPS menghantam komunitas FM karena hal itu tiba-tiba membuat banyak bukti sederhana dan memungkinkannya untuk mendekati masalah yang sangat kompleks. Dengan demikian, orang dapat bekerja dalam bahasa yang lebih ekspresif, karena sekarang masalah pernyataan ekspresif mulai diselesaikan. Kemajuan yang luar biasa terlihat jelas dalam proyek IronFleet : menggunakan pemecah SMT terbaik dan bahasa verifikasi tingkat lanjut, Microsoft mampu menulis 5.000 baris kode Dafny yang terbukti hanya dalam 3,7 orang-tahun! Ini adalah langkah yang sangat cepat: sebanyak empat baris penuh per hari (catatan: catatan sebelumnya milik seL4 , pengembang yang menulis dua baris sehari dalam C.

Buktinya sulit.

Mengapa ini dibutuhkan?

Saatnya untuk mundur dan bertanya: "Apa gunanya?" Kami mencoba membuktikan bahwa beberapa program memenuhi beberapa spesifikasi. Kebenaran adalah kisaran. Ada dua bagian untuk verifikasi: seberapa obyektif "memperbaiki" program Anda dan seberapa hati-hati Anda memeriksa kebenarannya. Jelas, semakin diverifikasi, semakin baik, tetapi verifikasi sepadan dengan waktu dan uang. Jika kami memiliki beberapa batasan (kinerja, waktu ke pasar, biaya, dll.), Validasi penuh belum tentu merupakan pilihan terbaik. Kemudian muncul pertanyaan, berapa cek minimum yang kita butuhkan dan berapa biayanya. Dalam kebanyakan kasus, misalnya, 90% atau 95% atau 99% kebenaran sudah cukup untuk Anda. Mungkin Anda harus menghabiskan waktu untuk memperbaiki antarmuka, daripada memeriksa 1% sisanya?

Lalu pertanyaannya: "Apakah cek 90/95/99% jauh lebih murah daripada 100%?" Jawabannya adalah ya. Cukup nyaman untuk mengatakan bahwa basis kode, yang kami uji dan ketik dengan baik, pada dasarnya benar kecuali untuk beberapa koreksi dalam produksi, dan kami bahkan menulis lebih dari empat baris kode per hari. Bahkan, sebagian besar kerusakan dalam sistem terdistribusi bisa dicegah dengan pengujian yang sedikit lebih komprehensif. Dan itu hanya perpanjangan dari tes, belum lagi fuzzing, pengujian berbasis properti, atau pengujian model. Anda bisa mendapatkan hasil yang benar-benar luar biasa dengan trik sederhana ini tanpa harus mendapatkan bukti penuh.

Bagaimana jika pengetikan dan pengujian tidak memberikan verifikasi yang memadai? Masih jauh lebih mudah untuk beralih dari 90% menjadi 99% daripada dari 99% menjadi 100%. Seperti disebutkan sebelumnya, Cleanroom adalah praktik pengembang yang mencakup dokumentasi komprehensif, analisis aliran menyeluruh, dan ulasan kode luas. Tidak ada bukti, tidak ada verifikasi formal, bahkan pengujian unit. Tetapi Cleanroom yang terorganisasi dengan baik mengurangi kepadatan cacat menjadi kurang dari 1 bug per 1000 baris kode dalam produksi (catatan: angka dari studi Stavley di Toward Zero-Defect Programming > tetapi selalu skeptis dan periksa sumbernya ). Memprogram Cleanroom tidak memperlambat laju perkembangan, dan tentunya berjalan lebih cepat dari 4 baris per hari. Dan Cleanroom sendiri hanyalah salah satu dari banyak metode pengembangan perangkat lunak yang sangat andal yang berada di antara pengembangan biasa dan verifikasi kode. Anda tidak perlu verifikasi lengkap untuk menulis perangkat lunak yang baik atau bahkan hampir sempurna. Ada saat-saat ketika dibutuhkan, tetapi bagi sebagian besar industri itu membuang-buang uang.

Namun, ini tidak berarti bahwa metode formal umumnya tidak ekonomis. Banyak metode yang sangat andal tersebut didasarkan pada spesifikasi penulisan kode yang tidak Anda buktikan secara formal. Dalam hal verifikasi, ada dua cara umum yang menguntungkan industri. Pertama, desain verifikasi alih-alih kode, yang akan kita bahas nanti. Kedua, sebagian verifikasi kode, yang akan kami pertimbangkan sekarang.

Verifikasi Kode Parsial

Untuk tugas sehari-hari, terlalu mahal untuk melakukan pemeriksaan penuh. Bagaimana dengan parsial? Lagi pula, Anda bisa mendapat manfaat dari bukti beberapa properti fragmen kode individual. Alih-alih membuktikan bahwa fungsi saya selalu mengurutkan angka dengan benar, saya setidaknya bisa membuktikan bahwa itu tidak berulang selamanya dan tidak pernah keluar dari jangkauan. Ini juga informasi yang sangat berguna. Jadi, bahkan bukti paling sederhana untuk program C adalah cara yang bagus untuk menghilangkan sebagian besar perilaku yang tidak terdefinisi .

Masalahnya adalah aksesibilitas .Sebagian besar bahasa dirancang untuk verifikasi penuh, atau tidak mendukungnya sama sekali. Dalam kasus pertama, Anda kehilangan banyak fitur bagus dari bahasa yang lebih ekspresif, dan dalam kasus kedua, Anda perlu cara untuk membuktikan hal-hal dalam bahasa yang memusuhi konsep itu sendiri. Untuk alasan ini, sebagian besar studi tentang verifikasi parsial fokus pada beberapa bahasa prioritas tinggi, seperti C dan Java. Banyak yang bekerja dengan himpunan bagian bahasa yang terbatas. Misalnya, SPARK adalah subset terbatas dari Ada, sehingga Anda dapat menulis kode SPARK kritis dan berinteraksi dengan kode Ada yang kurang kritis. Tetapi sebagian besar bahasa ini adalah ceruk yang cukup.

Lebih sering, jenis verifikasi tertentu tertanam dalam struktur dasar bahasa. Sistem tipifikasi yang digunakan dalam produksi adalah varian umum: Anda mungkin tidak tahu bahwa ekor selalu mengembalikan ekor, tetapi Anda tahu persis apa jenisnya [a] -> [a]. Ada juga contoh seperti Rust dengan keamanan memori terbukti dan Pony dengan bukti keamanan dengan pengecualian. Mereka sedikit berbeda dari SPARK dan Frama-C karena mereka hanya dapat melakukan pemeriksaan parsial. Dan mereka biasanya dikembangkan oleh para ahli dalam bahasa pemrograman, dan bukan ahli dalam metode formal: ada banyak kesamaan antara kedua disiplin ilmu, tetapi mereka tidak identik. Mungkin ini sebabnya bahasa seperti Rust dan Haskell sangat cocok untuk penggunaan praktis.

Spesifikasi desain

Sejauh ini, kami hanya berbicara tentang verifikasi kode. Namun, metode formal memiliki sisi lain, yang lebih abstrak dan memverifikasi desain itu sendiri, arsitektur proyek. Analisis ini sangat dalam sehingga identik dengan spesifikasi formal : jika seseorang mengatakan bahwa dia memenuhi spesifikasi formal, kemungkinan besar berarti dia mendefinisikan dan memverifikasi desain.

Seperti yang telah kami katakan, untuk membuktikan semua baris kode sangat, sangat sulit. Tetapi banyak masalah dalam produksi muncul bukan karena kode, tetapi karena interaksi komponen sistem. Jika kita mengabaikan detail implementasi, misalnya, menerima begitu saja bahwa sistem mampu mengenali burung, maka akan lebih mudah bagi kita untuk menganalisis bagaimana pohon dan burung masuk ke dalam desain keseluruhan sebagai modul tingkat tinggi. Pada skala seperti itu, menjadi jauh lebih mudah untuk menggambarkan hal-hal yang tidak dapat Anda sadari, seperti lingkungan runtime, interaksi manusia, atau aliran waktu tanpa ampun . Pada skala ini, kami memformalkan niat kami menggunakan sistem umum, bukan garis kode. Ini jauh lebih dekat ke tingkat manusia, di mana proyek dan persyaratan bisa jauh lebih ambigu daripada di tingkat kode.

Sebagai contoh, mari kita mengambil prosedur dengan spesifikasi kasar "jika itu disebut, itu membuat panggilan sistem untuk menyimpan data ke repositori dan memproses kesalahan sistem". Properti sulit untuk diverifikasi, tetapi cukup jelas bagaimana melakukan ini. Apakah data diserialisasi dengan benar? Apakah jaminan kami dilanggar karena input yang salah? Apakah kita menangani semua cara yang mungkin terjadi kegagalan panggilan sistem? Sekarang bandingkan sistem logging tingkat tinggi dengan spesifikasi "semua pesan dicatat" dan jawab pertanyaan-pertanyaan berikut:

Apakah semua pesan direkam atau semua pesan yang masuk ke sistem ? Pesan direkam sekali atau dijamin satu kali?
Bagaimana cara mengirim pesan? Apakah ini gilirannya? Apakah saluran mengirimkannya hanya sekali? Apakah semuanya baik-baik saja dengan pengiriman?
? , ? «» , ?
, ? ?
? « » ?
GDPR?
.

Tanpa desain formal, lebih sulit untuk mengungkapkan persyaratan yang benar-benar diperlukan untuk sistem. Jika Anda tidak dapat mengekspresikannya, maka Anda tidak tahu apakah desain benar-benar memenuhi persyaratan atau hanya terlihat seperti mereka, tetapi itu dapat menyebabkan konsekuensi yang tidak terduga. Dengan mengutarakan niat dan desain secara lebih formal, kita dapat dengan mudah memverifikasi bahwa kita sebenarnya mengembangkan apa yang kita butuhkan.

Sama seperti kita menggunakan bahasa pemrograman untuk mewakili kode, kita menggunakan bahasa spesifikasi untuk mewakili proyek. Bahasa spesifikasi biasanya berorientasi pada spesifikasi desain daripada spesifikasi kode, meskipun beberapa bahasa dapat digunakan untuk kedua kasus (catatan: proses penyesuaian spesifikasi desain dengan spesifikasi kode disebut penyempurnaanDi masa depan, saya akan memanggil bahasa spesifikasi bahasa desain (DL) untuk meminimalkan kebingungan (sekali lagi, ini bukan terminologi yang umum; kebanyakan orang menggunakan "bahasa spesifikasi", tapi saya ingin membedakan dengan jelas antara spesifikasi kode dan spesifikasi desain).

Mungkin DL penuh pertama adalah VDM sekitar tahun 1972. Sejak itu, kami telah melihat berbagai macam bahasa spesifikasi yang berbeda. Ruang DL jauh lebih beragam dan terfragmentasi daripada dengan bahasa verifikasi kode (CVL). Secara kasar, orang-orang menemukan DL sebagai sarana untuk mencapai tujuan, dan CVL sebagai tujuan itu sendiri. Karena mereka sangat dipengaruhi oleh bidang masalah tertentu, DL mengimplementasikan semua jenis ide dan semantik. Berikut ini adalah gambaran yang sangat, sangat singkat dari beberapa DLs pertama:

Bahasa	Area pemodelan	Berarti
Z	persyaratan bisnis	aljabar relasional
Promela		CSP
SDL		-

Karena DLs biasanya dibuat untuk memecahkan masalah tertentu, kebanyakan dari mereka memiliki setidaknya dua atau tiga aplikasi nyata. Sebagai aturan, hasilnya sangat positif. Praktisi mengatakan DL memberikan pemahaman tentang masalah dan membuat mencari solusi lebih mudah. Untuk waktu yang lama, juara utama adalah Praxis (sekarang Altran), yang menerapkan "fix-by-design" - kombinasi konstruksi-Z dan kode SPARK - untuk menciptakan sistem keamanan yang kritis. Spesifikasi menghemat waktu dan uang karena Anda tidak akan menemukan kesalahan desain pada tahap akhir proyek.

Pamela Zave bereksperimen dengan Alloy dan menemukan bug mendasar di Chord, salah satu tabel hash terdistribusi utama. AWS Mulai Menemukan Kesalahan Kritis 35 Langkahdengan menulis spesifikasi TLA +. Dalam pengalaman saya, ketika orang mencoba menulis spesifikasi, mereka segera menjadi penggemar bisnis ini.

Tetapi penggemar metode formal dan orang-orang dari luar sama sekali berbeda menilai nilai spesifikasi penulisan. Bagi penggemar, keuntungan terbesar adalah proses desain itu sendiri membuat Anda mengerti apa yang Anda tulis. Ketika Anda perlu secara formal mengungkapkan apa yang dilakukan sistem Anda, maka banyak kesalahan implisit tiba-tiba menjadi sangat jelas. Orang luar tidak bisa mengerti ini sama sekali. Jika Anda ingin mencoba DL seseorang, seseorang harus memiliki cara untuk memverifikasi bahwa desain benar-benar memiliki sifat yang ia inginkan.

Untungnya, ini juga sangat penting bagi banyak specifier, jadi verifikasi desain adalah bidang penelitian yang luas.

Pemeriksaan Model

Seperti halnya kode, kita dapat memverifikasi desain dengan menulis teorema. Untungnya, kami memiliki satu trik lagi: Anda dapat menggunakan program pemeriksa model. Alih-alih mengumpulkan bukti bahwa desain itu benar, kami hanya dengan kasar memaksa ruang kemungkinan negara dan melihat apakah ada negara yang salah di dalamnya. Jika kami tidak menemukan apa pun, maka semuanya baik-baik saja (catatan: program verifikasi model juga digunakan untuk memverifikasi kode, seperti JMBC, tetapi verifikasi model lebih sering digunakan dalam verifikasi desain daripada verifikasi kode).

Validasi model memiliki banyak keunggulan. Pertama, tidak perlu menulis bukti, yang menghemat banyak waktu dan tenaga. Kedua, tidak perlu belajarmenulis bukti, sehingga penghalang entri jauh lebih rendah. Ketiga, jika desain rusak, memeriksa model akan memberikan contoh tandingan eksplisit. Ini membuatnya jauh lebih mudah untuk memperbaiki kesalahan, terutama jika dibutuhkan 35 langkah untuk memperbanyaknya. Cobalah untuk menemukannya sendiri.

Ada beberapa kekurangan. Pertama-tama, alat-alat ini tidak begitu kuat. Secara khusus, Anda mungkin menemukan tidak terbatas(Tidak terikat) oleh model yang memiliki jumlah tak terbatas dari berbagai negara. Misalnya, Anda menetapkan penangan antrian pesan: biasanya berfungsi dengan daftar sepuluh pesan. Tetapi jika Anda perlu mempercayainya di daftar mana pun ... yah, ada jumlah tak terbatas dari mereka, sehingga model memiliki jumlah negara tak terbatas. Sebagian besar alat validasi model memiliki trik yang berbeda untuk situasi seperti itu, seperti mendefinisikan persamaan atau kelas simetri, tetapi setiap kasus berbeda.

Kelemahan lain besar - ledakan di ruang negara (state-space ledakan). Bayangkan Anda memiliki tiga proses, yang masing-masing terdiri dari empat langkah berurutan, dan mereka dapat mengubah langkah-langkah tersebut dengan cara apa pun. Jika mereka tidak mempengaruhi perilaku satu sama lain, maka ternyata(4*3)! / (4!)^3 = 34 650kemungkinan eksekusi (perilaku). Jika setiap proses memiliki satu dari lima keadaan awal, maka jumlah total perilaku meningkat menjadi 4.300.000, dan memeriksa model harus memastikan bahwa mereka semua berperilaku baik. Dan ini asalkan mereka tidak berinteraksi satu sama lain! Jika mereka mulai melakukan ini, ruang negara akan tumbuh lebih cepat. Ledakan kombinatorial dianggap sebagai masalah utama untuk model pengujian, dan masih banyak pekerjaan yang harus dilakukan untuk menyelesaikan masalah ini.

Tetapi pada saat yang sama, ada cara lain untuk menangani ledakan ruang negara: melemparkan lebih banyak peralatan ke dalamnya. Masalah terbesar untuk memeriksa model adalah "hanya" masalah kinerja, dan kami menyelesaikan masalah kinerja dengan sangat baik. Sebagian besar (tetapi tidak semua) pemeriksaan model mudah diparalelkan. Setelah mengoptimalkan model dan mengujinya dengan parameter kecil, Anda dapat menggunakan AWS cluster dan menjalankannya dengan parameter besar.

Dalam praktiknya, banyak kualifikasi menggunakan validasi model, dan kemudian, jika perlu, beralih ke program untuk membuktikan teorema (catatan: perlu diingat bahwa "banyak kualifikasi" sekitar sepuluh). Semakin banyak spesialis spesifikasi yang meluncurkan validasi model, dan ketika sudah mencapai batas kemampuannya, mereka beralih ke bentuk verifikasi yang kurang intensif.

Masalah Spesifikasi Desain

Dengan demikian, verifikasi desain lebih sederhana dan lebih cepat daripada verifikasi kode, dan telah menunjukkan banyak keberhasilan yang mengesankan. Jadi mengapa orang tidak menggunakannya? Masalah dengan DV jauh lebih berbahaya. Verifikasi kode adalah masalah teknis, dan verifikasi desain adalah masalah sosial: orang tidak melihat intinya.

Ini sebagian besar disebabkan oleh kenyataan bahwa desain bukan kode . Di sebagian besar DL, tidak ada cara otomatis untuk membuat kode, juga tidak ada cara untuk mengambil kode yang ada dan memeriksanya terhadap desain (catatan: pembuatan kode dari spesifikasi disebut sintesis ; untuk orientasi, lihat karya Nadya Polikarpova ; bukti bahwa kode cocok dengan spesifikasi (atau spesifikasi sesuai dengan spesifikasi lainnya) disebutklarifikasi : penelitian aktif sedang berlangsung di kedua arah).

Pemrogram cenderung tidak mempercayai artefak perangkat lunak yang bukan kode atau tidak dipaksa untuk menyinkronkan dengan kode. Untuk alasan yang sama, dokumentasi, komentar, grafik, wiki, dan commit sering diabaikan.

Tampaknya programmer tidak percaya bahwa spesifikasi dapat digunakan. Dalam pengalaman saya, mereka menyarankan bahwa alat saat ini (pseudo-code, diagram, TDD) lebih dari cukup untuk desain yang tepat. Saya tidak tahu seberapa luas pendapat ini dan saya tidak bisa menjelaskannya dengan apa pun selain konservatisme umum.

Tapi persis setiap komunitas metodologi memiliki keluhan yang saya tahu: Pendukung TDD mengeluh bahwa programmer tidak ingin mencoba TDD, penggemar Haskell mengeluh bahwa programmer tidak berpikir tentang pengetikan statis, dan sebagainya.

Saya mendengar argumen bahwa Agile tidak menerima desain yang dirancang sebelumnya, jadi tidak ada yang mau membuat spesifikasi formal. Mungkin Tetapi banyak orang yang saya temui menolak Agile dan FM. Argumen lain adalah bahwa metode formal historis secara konstan dievaluasi ulang dan tidak memenuhi apa yang dijanjikan. Ini juga mungkin, tetapi kebanyakan orang bahkan belum pernah mendengar tentang metode formal, dan bahkan lebih lagi tentang sejarah mereka.

Sangat sulit untuk membuat orang khawatir tentang apa yang belum mereka lakukan, bahkan jika mereka menyadari manfaatnya.

Ringkasan

Memverifikasi kode adalah tugas yang sulit. Semakin banyak orang terlibat, meskipun program pembuktian teorema dan pemecah SMT menjadi lebih kompleks. Tapi tetap saja, di masa mendatang, mungkin, ini akan tetap banyak spesialis.

Verifikasi desain jauh lebih sederhana, tetapi penggunaannya perlu mengatasi hambatan budaya. Saya pikir situasinya dapat diubah. Dua puluh tahun yang lalu, pengujian otomatis dan ulasan kode adalah topik yang cukup eksotis dan niche, tetapi akhirnya menjadi mainstream. Sekali lagi, pemrograman kontrak adalah niche dan tetap demikian.

Saya harap artikel ini menjelaskan sedikit lebih baik mengapa metode formal sangat jarang digunakan. Setidaknya ini adalah penjelasan yang lebih baik daripada argumen biasa "web bukan pesawat." Jangan ragu untuk berteriak jika Anda melihat kesalahan yang jelas.

Mengapa orang tidak menggunakan metode formal?