sturdy
1.0.0
Sturdy adalah perpustakaan untuk membuat analisis statis suara di Haskell. Analisis statis adalah alat yang menghasilkan informasi tentang program komputer tanpa benar -benar menjalankan program. Contoh analisis statis adalah pemeriksa jenis, pencari bug (misalnya Java FindBugs), analisis untuk keamanan (misalnya analisis noda), dan analisis yang digunakan untuk optimisasi kompiler.
Proyek ini berfokus pada analisis statis suara . Analisis statis terdengar jika hasil analisis mencerminkan perilaku runtime aktual dari program dan pengguna dapat mengandalkan hasilnya. Misalnya, jika analisis statis yang digunakan untuk optimisasi kompiler tidak sehat, optimasi dapat mengubah semantik program, yang mengarah pada perilaku yang tidak terduga saat runtime. Untuk tujuan ini, Sturdy mengikuti teori bukti kesehatan komposisi dari penafsir abstrak dan komponen suara dan dapat digunakan kembali untuk interpretasi abstrak untuk menyederhanakan bukti kesehatan analisis statis.
Kokoh memfaktorkan interpreter beton dan interpreter abstrak (analisis statis) menjadi penerjemah generik . Interpreter generik ini diparameterisasi oleh antarmuka yang mengandung operasi primitif yang menggambarkan semantik bahasa, seperti try , catch dan finally untuk pengecualian. Interpreter konkret dan abstrak kemudian instantiate interpreter generik dengan mengimplementasikan antarmuka ini. Reorganisasi ini tidak hanya memisahkan kekhawatiran yang berbeda dalam implementasi analisis statis, tetapi juga menyederhanakan bukti kesehatannya. Rincian lebih lanjut dapat ditemukan di kertas ICFP kami.
Sturdy memungkinkan untuk membangun analisis statis secara modular dari komponen analisis yang dapat digunakan kembali. Setiap komponen analisis merangkum masalah analisis tunggal dan dapat dibuktikan secara independen dari analisis di mana ia digunakan. Selain itu, komponen teori analisis menjamin bahwa analisis statis adalah suara, jika semua komponen analisisnya sehat. Ini berarti bahwa pengembang analisis tidak perlu khawatir tentang kesehatan selama mereka menggunakan kembali komponen analisis suara. Rincian lebih lanjut dapat ditemukan di koran Oopsla kami.
Untuk membangun, memasang alat Stack Build dan menjalankan stack build dari direktori root proyek.
Proyek yang kokoh saat ini berisi penafsir konkret dan abstrak dan generik untuk bahasa -bahasa berikut:
Untuk menjalankan tes bahasa tertentu menggunakan stack test sturdy-$(lang) , misalnya,
stack test sturdy-pcf
Algoritma FixPoint Berbasis Kombinator untuk Penerjemah Abstrak Langkah Besar
Sven Keidel, Sebastian Erdweg, Tobias Hombücher
Konferensi Internasional tentang Pemrograman Fungsional (ICFP). ACM, 2023. [PDF]
Penerjemah definisi abstrak modular untuk WebAssembly
Katharina Brandl, Sebastian Erdweg, Sven Keidel, Nils Hansen
Konferensi Eropa tentang Pemrograman Berorientasi Objek (ECOOP). ACM, 2023. [PDF]
Pendekatan sistematis untuk interpretasi abstrak transformasi program
Sven Keidel dan Sebastian Erdweg.
Verifikasi, Pemeriksaan Model, dan Interpretasi Abstrak (VMCAI). Springer, 2020. [PDF]
Komponen suara dan dapat digunakan kembali untuk interpretasi abstrak
Sven Keidel dan Sebastian Erdweg.
Pemrograman, sistem, bahasa, dan aplikasi yang berorientasi objek (OOPSLA). ACM, 2019 [PDF] [Bicara]
Bukti Kesehatan Komposisi dari Penerjemah Abstrak
Sven Keidel, Casper Bach Poulsen dan Sebastian Erdweg.
Konferensi Internasional tentang Pemrograman Fungsional (ICFP). ACM, 2018 [PDF] [Bicara]
Proyek yang kokoh adalah upaya bersama dari orang -orang berikut (dalam urutan abjad):
Casper Bach Poulsen, Jente Hidskes, Matthijs Bijman, Sarah Müller, Sebastian Erdweg, Sven Keidel, Tobias Hombücher, Wouter Raateland
