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

25

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.

Nathan BeDell
sumber

Jawaban:

13

Honda dan Yoshida

(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:

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 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.

Martin Berger
sumber
15

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.

cody
sumber
tanpa terlalu banyak kesulitan - tidak juga. Idris ketat secara default, dan Haskell malas; itu saja merupakan masalah utama. Kompatibilitas dengan Haskell juga tidak pernah menjadi prioritas yang sangat tinggi untuk desain Idris.
Bartek Banachewicz
Cukup adil. Agda memeriksa penghentian secara default, jadi hal-hal seperti ketat bukan masalah dalam teori . Tentu saja run-time bisa sangat berbeda.
cody
8

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 .

Ohad Kammar
sumber
1

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.

Sam Tobin-Hochstadt
sumber