Apakah ada sistem verifikasi formal beranotasi untuk bahasa pemrograman fungsional murni?

ACSL (Ansi C Spesifikasi Bahasa), adalah spesifikasi untuk kode C, dijelaskan dengan komentar khusus, yang memungkinkan kode C untuk diverifikasi secara resmi.

Saya belum memeriksanya, tetapi saya membayangkan bahwa metode formal yang digunakan dalam verifier ACSL akan mirip dengan Hoare Logic. Untuk bahasa fungsional murni, seperti Haskell, saya tidak bisa membayangkan formalisme seperti apa yang akan digunakan untuk verifikasi formal.

Adakah yang membuat sesuatu yang mirip dengan ACSL , tetapi untuk bahasa fungsional murni? Jika tidak, apakah ada penelitian tentang verifikasi formal gaya-keterangan beranotasi untuk bahasa fungsional?

Saya tahu bahwa ada pengetikan dependen, yang didukung banyak bahasa (Agda, Idris, dll ...), tetapi dalam pengetikan bergantung Haskell sulit tanpa melakukan beberapa jenis-sihir (tidak dapat dibaca?). Dengan mengingat hal itu, dan karena Haskell memiliki dukungan perpustakaan yang jauh lebih baik daripada Agda dan Idris, saya percaya sistem semacam itu untuk verifikasi formal fungsional mungkin berguna, tetapi saya tidak tahu apakah penelitian telah dilakukan tentang ini atau tidak.

Honda dan Yoshida

• Logika Program Komposisi untuk Fungsi Orde Tinggi Polimorfik

(mungkin) memelopori logika Hoare untuk bahasa yang murni fungsional. Karya ini didasarkan pada logika Hennessy-Milner dan pengkodean fungsi Milner ke dalam proses, seperti dijelaskan di sini:

• Dari Logika Proses ke Logika Program

Karya Régis-Gianas et al yang disebutkan dalam jawaban lain mirip dengan karya pertama di atas oleh Honda / Yoshida. Ini telah diperluas ke bahasa gaya ML yang efektif:

• Logika Program yang Lengkap Secara Observasional untuk Fungsi Imperatif Tingkat Tinggi

• Sebuah Analisis Logika tentang Aliasing dalam Fungsi Imperatif Tingkat Tinggi

• Penalaran Logis Untuk Fungsi Tingkat Tinggi Dengan Negara Bagian

• Logika Program untuk Kontrol Urutan Tinggi Urutan

• Logika Program untuk Meta-Programming Homogen

Logika yang disebutkan adalah apa yang disebut observasi lengkap, artinya operasional dan semantik logis terjadi bersamaan. Arthur Charguéraud menggunakan pelengkap ini untuk karyanya memverifikasi program fungsional bergaya Hoare di Coq.

$F^*$

Tampaknya ada korespondensi yang erat antara jenis perbaikan dan ACSL seperti notasi.

Akhirnya saya hanya bisa menyarankan untuk melihat Agda dan Idris lebih dekat, karena mereka dapat dikompilasi ke Haskell, dan bertujuan untuk menyediakan pengguna dengan bahasa pemrograman yang dapat digunakan (terutama Idris). Saya menduga mungkin untuk mengintegrasikan perpustakaan Haskell ke dalam kode Idris tanpa terlalu banyak kesulitan.

Lihat juga tesis Yann Régis-Gianas PhD bekerja dengan François Pottier: A Hoare Logic untuk Program Fungsional Call-by-Value (MPC'08) . Pekerjaan ini diperluas untuk mencakup efek samping ML yang biasa dilakukan oleh Johannes Kanig dan Jean-Cristophe Filliatre pada tahun 2009: Who: A Verifier untuk Program Tingkat Tinggi yang Efektif .

Ada makalah di tahun ini ICFP , tipe penyempurnaan untuk Haskell . Makalah ini membahas penghentian memeriksa daripada logika Hoare penuh, tapi mudah-mudahan itu adalah awal dari arah ini.

Bagian kerja terkait dalam makalah itu berisi beberapa petunjuk, seperti Xu, Peyton-Jones, dan kontrak statis Claessen memeriksa Haskell , dan Sonnex, Drossopoulou, dan Zeno dan Vytiniotis Eisenbach, Peyton-Jones, Claessen, dan Halo Rosen .

Pekerjaan kami terkait verifikasi lunak kontrak, di OOPSLA 2012 dan ICFP 2014 , memungkinkan Anda untuk menulis kontrak, yang sangat mirip dengan spesifikasi ACSL, dan kemudian memverifikasi secara statis atau menggunakannya untuk memeriksa dinamis saat runtime.