Metode formal dapat digunakan untuk menentukan, membuktikan, dan menghasilkan kode untuk suatu aplikasi. Ini kurang rentan terhadap kesalahan - sehingga sebagian besar digunakan dalam program keselamatan / kritis.
Mengapa kita tidak menggunakannya lebih sering untuk pemrograman sehari-hari, atau dalam aplikasi web, dll ...?
Referensi :
Jawaban:
Insinyur adalah orang yang dapat melakukan dengan dolar apa yang dapat dilakukan orang bodoh dengan 10.
Kendala sumber daya, kendala anggaran, kendala waktu, semuanya penting.
Mengembangkan perangkat lunak menggunakan metode formal biasanya jauh lebih mahal dan memakan waktu lebih lama daripada tanpa. Juga, untuk banyak proyek, bagian tersulit adalah memahami persyaratan bisnis. Semua yang menggunakan metode formal membeli Anda dalam kasus itu adalah bukti bahwa kode Anda sesuai 100% dengan pemahaman Anda yang tidak lengkap dan salah tentang persyaratan bisnis.
Untuk alasan itu, penggunaan metode formal, bukti, verifikasi program, dan teknik serupa biasanya terbatas pada "hal-hal yang penting", yaitu perangkat lunak avionik, sistem kontrol untuk peralatan medis, pembangkit listrik, dll.
sumber
(-1 + 1) + INT_MAX = INT_MAX,-1 + (1 + INT_MAX)adalah perilaku undefined.Memprogram atau tidak memprogram?
Untuk memecahkan masalah dengan produk perangkat lunak, setelah memiliki pemahaman tentang persyaratan, Anda dapat BAIK menulis program menggunakan bahasa pemrograman ATAU menentukan program menggunakan bahasa formal dan menggunakan alat penghasil kode. Yang terakhir hanya menambah tingkat abstraksi.
Melakukan hal yang benar atau melakukan hal yang benar?
Pendekatan formal memberi Anda bukti bahwa perangkat lunak Anda bekerja sesuai dengan spesifikasi. Jadi produk Anda melakukan hal yang benar. Tetapi apakah itu melakukan hal yang benar?
Persyaratan tempat Anda bekerja mungkin tidak lengkap atau ambigu. Mereka bahkan bisa menjadi buggy. Dalam kasus terburuk, kebutuhan nyata bahkan tidak diungkapkan. Tetapi gambar bernilai ribuan kata, hanya gambar google untuk "Apa yang diinginkan pelanggan", misalnya dari artikel ini :
Biaya formalitas
Di dunia yang sempurna, Anda akan memiliki persyaratan yang sepenuhnya terperinci dan sempurna sejak awal. Anda kemudian dapat sepenuhnya menentukan perangkat lunak Anda. Jika Anda ingin formal, kode Anda akan dihasilkan secara otomatis sehingga Anda akan lebih produktif. Keuntungan produktivitas akan mengimbangi biaya alat formal. Dan semua orang sekarang akan menggunakan metode formal. Jadi mengapa tidak?
Dalam praktiknya, ini jarang kenyataan! Inilah sebabnya mengapa begitu banyak proyek air terjun gagal, dan mengapa metode pengembangan berulang (tangkas, RAD, dll) memimpin: mereka dapat menangani persyaratan, desain dan implementasi yang tidak lengkap dan tidak sempurna dan menyempurnakannya sampai mereka baik-baik saja.
Dan inilah intinya. Dengan metode formal, setiap iterasi harus memiliki spesifikasi formal yang sepenuhnya konsisten. Ini membutuhkan pemikiran yang cermat dan pekerjaan tambahan, karena logika formal tidak memaafkan dan tidak menyukai pikiran yang tidak lengkap. Eksperimen pembuangan sederhana menjadi mahal di bawah batasan ini. Dan begitu juga setiap iterasi yang akan mengarah ke pengulangan (misalnya ide yang tidak berhasil, atau persyaratan yang disalahpahami).
Dalam praktek
Ketika tidak diwajibkan untuk menggunakan metode formal untuk alasan hukum atau kontrak, Anda juga dapat mencapai kualitas yang sangat tinggi tanpa sistem formal, misalnya dengan menggunakan pemrograman berbasis kontrak dan praktik-praktik baik lainnya (mis. Tinjauan kode, TDD , dll ...). Anda tidak akan dapat membuktikan bahwa perangkat lunak Anda berfungsi, tetapi pengguna Anda akan menikmati kerja perangkat lunak lebih cepat.
Pembaruan: upaya yang terukur
Dalam edisi Oktober 2018 tentang Komunikasi ACM ada artikel menarik tentang perangkat lunak yang diverifikasi secara formal di dunia nyata dengan beberapa perkiraan upaya.
Menariknya (berdasarkan pengembangan OS untuk peralatan militer), tampaknya memproduksi perangkat lunak yang terbukti secara formal membutuhkan upaya 3,3 kali lebih banyak daripada dengan teknik teknik tradisional. Jadi itu sangat mahal.
Di sisi lain, ini membutuhkan upaya 2,3 kali lebih sedikit untuk mendapatkan perangkat lunak keamanan tinggi dengan cara ini dibandingkan dengan perangkat lunak yang direkayasa secara tradisional jika Anda menambahkan upaya untuk membuat perangkat lunak tersebut disertifikasi pada tingkat keamanan yang tinggi (EAL 7). Jadi jika Anda memiliki keandalan atau persyaratan keamanan yang tinggi pasti ada kasus bisnis untuk menjadi formal.
sumber
Setiap program dalam bahasa apa pun dapat dianggap sebagai spesifikasi formal (setara dengan beberapa mesin pemutar). 'Spesifikasi formal' tingkat tinggi mana pun untuk digunakan dalam membuktikan kebenaran formal juga - hanyalah program lain. Tetapi (biasanya) program yang buruk, tidak lengkap, tidak jelas, tidak cukup dipikirkan. Dan tidak secara kebetulan, biasanya ditulis oleh orang-orang yang tidak tahu cara memprogram (mereka biasanya ahli domain).
Dan dengan demikian membuktikan bahwa satu program kompatibel (menghasilkan jawaban yang sama atau bagaimana pun Anda mengkarakteristikkannya) dengan persyaratan formal tingkat tinggi, yang tidak berubah adalah bagaimana Anda menyelesaikan ambiguitas dalam spesifikasi formal tingkat tinggi. Tidak ada cara tujuan umum yang baik untuk melakukan itu.
Pemetaan persyaratan tingkat tinggi ke detail tingkat lebih rendah adalah inti dari apa sebenarnya pemrograman itu. Seharusnya tidak mengherankan bahwa pekerjaan inti yang dilakukan oleh seorang programmer membaca dan menafsirkan spesifikasi tidak dapat diganti dengan melambaikan tangan dan mengatakan 'sekarang lihat saja apakah spesifikasi formal tingkat tinggi ini dipenuhi oleh program sampel ini'.
Bahkan pada hari-hari awal pemrograman logika, di mana konsep ini pertama kali tampak begitu menjanjikan (karena baik spesifikasi tingkat tinggi dan program yang mendasari sebenarnya dapat ditulis dalam bahasa yang sama), masalah inti ini terbukti tidak bisa diselesaikan.
sumber