Jika Anda mempelajari metode formal untuk perangkat lunak, seberapa bermanfaatkah Anda menemukannya?

Jika Anda telah dilatih dalam penggunaan metode formal (FM) untuk pemrograman:

• Seberapa bermanfaatkah Anda menemukannya?
• Apa yang melibatkan pelatihan FM Anda (misalnya kursus, buku)?
• Alat FM apa yang Anda gunakan?
• Apa kelebihan dalam kecepatan / kualitas yang telah Anda berikan dibandingkan dengan tidak menggunakan FM?
• Perangkat lunak apa yang Anda buat dengan FM?
• Dan jika Anda tidak langsung menggunakan FM sekarang, apakah itu setidaknya layak untuk dipelajari ??

Saya ingin tahu banyak pengalaman / pendapat tentang FM yang dapat ditemukan di komunitas ini; Saya mulai membacanya dan ingin tahu lebih banyak.

Latar Belakang

Pemrograman dan pengembangan / rekayasa perangkat lunak adalah beberapa keterampilan / profesi manusia terbaru di Bumi, sehingga tidak mengherankan, bidang ini belum matang - yang ditampilkan dalam output utama bidang kami, karena kode yang biasanya terlambat dan rawan kesalahan. Ketidakdewasaan industri juga ditunjukkan oleh margin yang lebar (setidaknya 10: 1) dalam produktivitas antara rata-rata dan pembuat kode teratas. Fakta-fakta suram seperti itu tercakup dengan baik dalam literatur, dan diperkenalkan oleh buku-buku seperti Code Complete Steve McConnell .

Penggunaan metode formal (FM) telah diusulkan oleh tokoh-tokoh utama dalam perangkat lunak / CS (misalnya almarhum E. Dijkstra ) untuk mengatasi (salah satu) akar penyebab kesalahan: kurangnya ketelitian matematika dalam pemrograman. Dijkstra, misalnya, mengadvokasi siswa mengembangkan program dan buktinya bersama .

FM tampaknya jauh lebih lazim dalam kurikulum CS di Eropa dibandingkan dengan AS. Namun dalam beberapa tahun terakhir, pendekatan dan alat FM "ringan" baru seperti Alloy telah menarik perhatian. Tetap saja, FM masih jauh dari penggunaan umum di industri, dan saya berharap untuk umpan balik di sini tentang mengapa.

Memperbarui

Sampai sekarang (14/10/2010), dari 6 jawaban di bawah ini, tidak ada yang jelas berargumen untuk penggunaan FM dalam pekerjaan "dunia nyata". Saya benar-benar ingin tahu apakah seseorang bisa dan mau; atau mungkin FM benar-benar menggambarkan kesenjangan antara akademisi (FM adalah masa depan!) dan industri (FM sebagian besar tidak berguna).

Sama sekali tidak berguna untuk hal-hal yang tidak penting.

Saya memiliki kursus yang disebut, dengan tepat, "Metode Formal" yang berfokus pada Alloy - saya tidak mungkin melihat menggunakannya di mana pun. Punya kelas lain yang berfokus pada pemodelan konkurensi dengan LTSA - sama-sama tidak berguna.

Masalahnya adalah bahwa sebagian besar bug dan masalah dalam perangkat lunak (setidaknya dalam pengalaman saya) muncul dari kompleksitas yang terjadi di bawah tingkat abstraksi alat-alat tersebut.

Saya memiliki latar belakang dalam CSP (Communicating Sequential Processes). Bukan untuk membunyikan klakson saya sendiri, tetapi saya menulis tesis Master saya tentang CSP Jangka Waktu, khususnya "menyusun" spesifikasi yang ditulis dalam metode formal ke dalam C ++ yang dapat dieksekusi. Saya dapat mengatakan saya memiliki pengalaman dengan metode formal. Setelah saya menyelesaikan gelar saya dan mendapatkan pekerjaan di industri ini, saya belum menggunakan metode formal sama sekali. Metode formal masih terlalu teoritis untuk diterapkan di industri. Metode formal telah menemukan beberapa aplikasi praktis di bidang sistem embedded. Sebagai contoh, NASA menggunakan metode formal dalam proyek mereka. Saya akan berspekulasi bahwa metode formal sangat jauh dari yang diadopsi secara luas di industri. Sama sekali tidak masuk akal untuk menulis spesifikasi perangkat lunak dalam metode formal dan kemudian "menafsirkan manusia" ke dalam kerangka pilihan Anda. Bahasa Inggris dan diagram polos berfungsi lebih baik untuk itu, sementara tes unit dan integrasi telah melakukan pekerjaan yang cukup baik untuk "memverifikasi" kebenaran kode. kupikirmetode formal akan tetap di dunia akademis selama beberapa waktu .

State diagram dan Petri nets berguna untuk memodelkan dan menganalisis protokol dan sistem waktu nyata. Pertama, mereka membantu merancang solusi. Kedua, mereka membantu menemukan kasus uji untuk perangkat lunak yang menarik dalam situasi yang sangat spesifik.

Saya sudah membaca beberapa buku tentang metode formal, dan menerapkan beberapa. Reaksi langsung saya adalah, "Wah, buku-buku ini memberi tahu saya bagaimana menjadi programmer yang baik, selama saya seorang ahli matematika yang sempurna." Kelemahan lain adalah Anda hanya dapat membuktikan kesetaraan dengan deskripsi formal lainnya. Menulis spesifikasi formal untuk sebuah program sama dengan menulis sebuah program dalam bahasa tingkat yang lebih tinggi, dan tidak ada cara Anda dapat menghindari memperkenalkan bug dalam spesifikasi yang cukup besar.

Saya tidak pernah membuat metode formal bekerja dalam skala besar. Mereka dapat berguna untuk mendapatkan sesuatu yang kecil dan rumit yang benar, dan meyakinkan saya bahwa mereka benar. Dengan cara itu, saya dapat bekerja dengan balok bangunan yang sedikit lebih besar dan kadang-kadang sedikit lebih banyak dilakukan.

Satu hal yang saya ambil yang lebih bermanfaat secara umum adalah konsep invarian, pernyataan tentang program dan statusnya yang selalu benar. Apa pun yang Anda dapat alasannya baik.

Seperti disinggung di atas, saya bukan ahli matematika yang sempurna, jadi bukti saya terkadang mengandung kesalahan. Namun, dalam pengalaman saya, ini cenderung merupakan kesalahan besar yang mudah ditangkap dan diperbaiki.

Saya mengambil kursus pascasarjana dalam analisis program formal, di mana kami fokus pada semantik operasional. Saya melakukan tugas akhir saya tentang upaya seL4, meninjau metode formal yang mereka gunakan. Nilai utama saya dalam hal kepraktisan adalah nilai marginalnya. Anda tidak hanya harus menulis program, Anda harus menulis buktinya. Wow. Dua sumber bug. Bukan hanya satu. Lebih lanjut, ada sejumlah besar pembatasan yang ditempatkan pada kode aktual. Sangat sulit menggambarkan komputer fisik secara formal, termasuk I / O.

Belajar sendiri TLA + tahun lalu, telah menggunakannya sejak saat itu. Ini adalah salah satu alat pertama yang saya raih ketika saya memulai sebuah proyek. Kesalahan yang dilakukan kebanyakan orang adalah mereka menganggap bahwa metode formal adalah hal yang sepenuhnya atau tidak sama sekali: apakah Anda tidak menggunakan metode formal atau Anda memiliki verifikasi lengkap. Namun, ada sesuatu di antara mereka: spesifikasi formal , di mana Anda memeriksa bahwa spesifikasi abstrak proyek Anda tidak merusak invarian Anda. Tidak seperti verifikasi, spesifikasi cukup praktis untuk digunakan dalam industri.

Bahasa spesifikasi lebih ekspresif daripada bahasa pemrograman. Sebagai contoh, berikut adalah spec PlusCal (sangat) sederhana untuk penyimpanan data terdistribusi:

process node \in 1..5 \* Nodes
variables online = TRUE,
          stored \in SUBSET data; \* Some set
begin 
  Transfer:
    either
      with node \in Nodes, datum \in stored do
        node.stored := node.stored \union {datum};
      end
    or \* crash
      online := FALSE;
    end either;
end process;

Cuplikan ini menetapkan lima node yang berjalan secara bersamaan, menjalankan transfer dalam urutan arbitrer, di mana setiap transfer merupakan bagian data yang arbitrer ke node arbitrer. Selain itu, kami telah menetapkan bahwa transfer yang diberikan mungkin gagal dan menyebabkan simpul macet. Dan kita dapat mensimulasikan semua perilaku ini di pemeriksa model TLA +! Dengan begitu kita dapat menguji itu terlepas dari pesanan, tingkat kegagalan, dll, persyaratan kita masih berlaku. Omong-omong, mari kita tambahkan beberapa persyaratan. Pertama, kami tidak pernah mentransfer data ke simpul offline:

[][\A node \in Nodes: ~online => UNCHANGED node.stored]_vars

Dalam versi sederhana kami, pemeriksa model akan menemukan keadaan gagal. Kami juga dapat menentukan "setiap bagian data yang ada dalam setidaknya satu simpul online":

\A d \in data: \E n \in Nodes: n.online /\ d \in n.stored

Yang juga akan gagal. Selamat mencoba memeriksa ini dengan unit test!

Batasan utama spesifikasi adalah keberadaannya secara independen dari kode aktual Anda. Itu hanya bisa memberi tahu Anda bahwa desain Anda benar, bukan bahwa Anda menerapkannya dengan benar. Tetapi lebih cepat untuk menentukan daripada memverifikasi dan menangkap bug yang terlalu halus untuk pengujian, jadi saya merasa sepadan dengan usaha. Hampir semua kode yang melibatkan konkurensi atau banyak sistem adalah tempat yang baik untuk spesifikasi formal.

Saya dulu bekerja di departemen di ICL, sebelum mereka dibeli oleh Fujitsu. Mereka memiliki beberapa kontrak besar pemerintah yang membutuhkan bukti bahwa perangkat lunak berfungsi seperti yang diiklankan, jadi mereka membangun sebuah mesin yang akan mengambil spesifikasi formal yang ditulis dalam Z dan memvalidasi kode saat dijalankan, dengan lampu hijau atau merah besar untuk lulus / gagal.

Itu adalah hal yang luar biasa, tetapi, seperti yang ditunjukkan oleh @FishToaster yang terhormat , itu tidak berguna untuk apa pun yang tidak sepele.

1. " Seberapa berguna Anda menemukannya? "

Aplikasi Petri Nets untuk pemrograman komputer sangat berguna. Saya menciptakan "Elemen Bersih dan Anotasi", sebuah metode berdasarkan Petri Nets (Chionglo, 2014). Saya telah menerapkan metode ini sejak 2014 untuk menulis program JavaScript yang menggunakan Acrobat / JavaScript API untuk aplikasi formulir PDF.

2. “ Apa yang melibatkan pelatihan FM Anda (misalnya kursus, buku)?”

Saya “dilatih” tentang Petri Nets melalui belajar mandiri. Saya membaca bab-bab tentang Petri Nets dari buku teks “Petri Nets and Grafcet: Alat untuk Pemodelan Sistem Acara Diskrit” (David dan Alla, 1992). Saya juga telah membaca makalah penelitian tentang Petri Nets. Setelah membuat dan mendokumentasikan "Elemen dan Anotasi Bersih", saya berlatih menerapkan metode ini selama beberapa minggu.

3. “ Alat FM apa yang Anda gunakan?”

Saya menggambar diagram Petri Net menggunakan PowerPoint. Saya membuat tampilan formulir anotasi menggunakan Word. Saya membuat token game sebagai aplikasi formulir PDF menggunakan Acrobat dan Notepad juga. Setelah menambahkan entri ke dalam bentuk terjemahan dari entri-entri ini ke dalam kode JavaScript adalah sistematis. Dengan demikian, terjemahan harus dimungkinkan. Jika "entri" ditambahkan ke objek grafik di PowerPoint maka mungkin juga mungkin untuk menerjemahkannya secara sistematis ke dalam kode JavaScript dan untuk mengotomatisasi terjemahan ini juga. Saya juga menggunakan seperangkat alat dalam proses yang melakukan terjemahan ini dan untuk membuat sumber daya tambahan untuk membuat aplikasi formulir PDF (Chionglo, 2018; 2017).

4. “ Apa kelebihan dalam kecepatan / kualitas yang Anda berikan dibandingkan dengan tidak menggunakan FM?”

Saya dapat menulis program JavaScript menggunakan "Elemen dan Anotasi Net" lebih cepat daripada saya dapat menulis program JavaScript tanpa menggunakan "Elemen dan Anotasi Net". Dan untuk program-program besar saya dapat menghentikan pengkodean dan kembali ke pengkodean nanti (atau lebih kemudian) tanpa bertanya-tanya di mana untuk melanjutkan (Chionglo, 2019). Dalam beberapa kasus saya dapat menulis program JavaScript menggunakan "Elemen dan Anotasi Net" tetapi tidak dapat menulis program JavaScript tanpa menggunakan "Elemen dan Anotasi Net". Misalnya saya tidak bisa membuat implementasi fungsi rekursif non-rekursif tanpa menggunakan "Elemen dan Anotasi Bersih" (Chionglo, 2019b; 2018b; 2016). Ini benar dengan atau tanpa alat dalam proses.

5. " Perangkat lunak apa yang Anda buat dengan FM? "

Saya menggunakan "Elemen dan Anotasi Bersih" untuk membuat program JavaScript yang menggunakan Acrobat / JavaScript API untuk aplikasi formulir PDF. Saya juga dapat menerapkan metode untuk membuat program JavaScript untuk dokumen HTML dan membuat Sketsa Arduino (Chionglo, 2019c; 2019d).

6. " Dan jika Anda tidak secara langsung menggunakan FM sekarang, apakah itu setidaknya layak dipelajari? "

Referensi

Chionglo, JF (2019b). Menghitung Jangka Waktu Ke-N dari Relasi Rekursif: Menggunakan Fungsi Non-Rekursif - Jawaban untuk Pertanyaan di Stack Exchange Matematika. < https://www.academia.edu/38496025/Computing_the_N-th_Term_of_a_Recursive_Relation_Using_a_Non-Recursive_Function_A_Reply_to_a_Question_at_Mathematics_Stack_Exchange >.

Chionglo, JF (2019c). Logika Kontrol Efek Api, Simulasi, dan Sketsa: Jawaban atas Permintaan di Forum Komunitas Arduino.https://www.academia.edu/40342956/Flame_Effect_Control_Logic_Simulation_and_Sketch_A_Reply_to_a_Request_at_the_Arduino_Community_Forum .

Chionglo, JF (2019). Bagaimana Saya Terus Mengkode Aplikasi setelah Istirahat yang Lama? Membalas "Bagaimana Anda tahu di mana Anda berhenti dalam kode Anda setelah istirahat 2 minggu?" - Rekayasa Perangkat Lunak Stack Exchange. https://www.academia.edu/39705042/How_I_Continue_Coding_an_Application_after_a_Long_Break_Reply_to_How_do_you_know_where_you_stopped_in_your_codes_after_a_2-week_break_Software_Engineering_Stack_Exchange .

Chionglo, JF (2019d). Logika Kontrol Tampilkan-dan-Sembunyikan: Terinspirasi oleh Pertanyaan di Stack Overflow. < https://www.academia.edu/40283015/Show-and-Hide_Control_Logic_Inspired_by_a_Question_at_Stack_Overflow >.

Chionglo, JF (2018b). Model Petri Net untuk Faktorial Angka: Dan Fungsi JavaScript Non-Rekursif untuk Menghitungnya. <>.

Chionglo, JF (2018). Buat Hyper Form ™ - Alur Kerja yang Sedang Berjalan: Pembaruan pada Penelitian Pemrograman Net. https://www.academia.edu/37697498/Create_Hyper_Form_-A_Workflow_in_Progress_Update_on_the_Net_Programming_Research .

Chionglo, JF (2017). Pemrograman Net: Proposal Penelitian: Untuk Mengembangkan Aplikasi Formulir PDF dengan PowerPoint dan Acrobat. https://www.academia.edu/33374809/Net_Programming_A_Research_Proposal_For_Developing_PDF_Form_Applications_with_PowerPoint_and_Acrobat. .

Chionglo, JF (2016). Model Petri Net untuk Menghitung Angka Fibonacci. https://www.academia.edu/31748108/A_Petri_Net_Model_for_Computing_the_Fibonacci_Number.

Chionglo, JF (2014). Elemen dan Anotasi Bersih untuk Pemrograman Komputer: Komputasi dan Interaksi dalam PDF. https://www.academia.edu/26906314/Net_Elements_and_Annotations_for_Computer_Programming_Computations_and_Interactions_in_PDF .

David, R. dan H. Alla. (1992). Petri Nets and Grafcet: Alat untuk Pemodelan Sistem Event-Diskrit. Upper Saddle, NJ: Prentice Hall.