Apakah ada alternatif untuk jenis analisis statis?

Mengetik statis dalam bahasa pemrograman dapat membantu untuk menegakkan jaminan tertentu pada waktu kompilasi - tetapi apakah mengetikkan satu-satunya alat untuk pekerjaan ini? Apakah ada cara lain untuk menentukan invarian?

Misalnya, bahasa atau lingkungan dapat membantu menegakkan jaminan tentang panjang array, atau tentang hubungan antara input ke suatu fungsi. Saya hanya belum pernah mendengar hal seperti ini di luar sistem tipe.

Suatu hal terkait yang saya ingin tanyakan adalah apakah ada cara non-deklaratif untuk melakukan analisis statis (sebagian besar tipe deklaratif, sebagian besar ).

Sistem tipe statis adalah jenis analisis statis, tetapi ada banyak analisis statis yang umumnya tidak dikodekan dalam sistem tipe. Sebagai contoh:

• Pengecekan model adalah teknik analisis dan verifikasi untuk sistem konkuren yang memungkinkan Anda membuktikan bahwa program Anda berperilaku baik di bawah semua kemungkinan interleaving thread.

• Analisis aliran data mengumpulkan informasi tentang nilai-nilai variabel yang mungkin, yang dapat menentukan apakah beberapa komputasi berlebihan, atau beberapa kesalahan tidak diperhitungkan.

• Interpretasi abstrak memodelkan efek program secara konservatif, biasanya sedemikian rupa sehingga analisis dijamin akan berakhir — pemeriksa tipe dapat diimplementasikan dengan cara yang mirip dengan interpreter abstrak.

• Pemisahan logika adalah logika program (digunakan misalnya dalam penganalisa Infer ) yang dapat digunakan untuk alasan tentang status program, dan mengidentifikasi masalah seperti null pointer dereferences, state tidak valid, dan kebocoran sumber daya.

• Pemrograman berbasis kontrak adalah cara untuk menentukan prasyarat, postkondisi, efek samping, dan invarian. Ada memiliki dukungan asli untuk kontrak dan dapat memverifikasi beberapa dari mereka secara statis.

Kompiler pengoptimalisasi melakukan banyak analisis kecil untuk membangun struktur data menengah untuk digunakan selama optimasi — seperti SSA, perkiraan biaya inlining, informasi pemasangan pasangan instruksi, dan sebagainya.

Contoh lain dari analisis statis non-deklaratif ditemukan di Hack typechecker, di mana yang normal konstruksi kontrol aliran dapat memperbaiki jenis variabel:

$x = get_value();
if ($x !== null) {
    $x->method();    // Typechecks because $x is known to be non-null.
} else {
    $x->method();    // Does not typecheck.
}

Dan berbicara tentang "pemurnian", di tanah sistem tipe, tipe pemurnian (seperti yang digunakan dalam LiquidHaskell ) memasangkan tipe dengan predikat yang dijamin tahan untuk contoh tipe "halus". Dan tipe dependen mengambil ini lebih jauh, memungkinkan tipe bergantung pada nilai. "Halo dunia" dari pengetikan dependen biasanya fungsi penggabungan array:

(++) : (a : Type) -> (m n : Nat) -> Vec a m -> Vec a n -> Vec a (m + n)

Di sini, ++mengambil dua operan tipe Vec a mdan Vec a n, menjadi vektor dengan tipe elemen adan panjangnya masing m- nmasing, yang merupakan bilangan asli ( Nat). Ini mengembalikan vektor dengan tipe elemen yang sama yang panjangnya m + n. Dan fungsi ini membuktikan batasan ini secara abstrak, tanpa mengetahui nilai spesifik mdan n, sehingga panjang vektor mungkin dinamis.

@ JonPurdy menjawab lebih baik, tetapi saya ingin menambahkan beberapa contoh lagi:

Jelas:

• pemeriksaan sintaks

• linting

Tidak jelas:

• Rust memungkinkan programmer untuk menentukan apakah "binding" bisa diubah , dan memberlakukan batasan ini.

• Ini semacam terkait: beberapa bahasa mengaktifkan beberapa kode untuk dijalankan pada waktu kompilasi, yang berarti bahwa banyak hal yang akan menjadi kesalahan runtime dapat ditangkap pada waktu kompilasi. Beberapa contohnya adalah makro dan prosedur bahasa Nim yang ditandai dengan compileTimepragma .

• Pemrograman logika pada dasarnya membangun sebuah program dengan memberikan pernyataan.

Pengetikan semi-statis:

• Facebook's Flow memungkinkan hibrida antara pengetikan dinamis dan statis. Idenya adalah bahwa kode dinamis pun diketik secara implisit. Flow memungkinkan Anda menjalankan server yang mengawasi kode Anda saat dijalankan untuk mendeteksi kemungkinan kesalahan ketik, bahkan jika Anda tidak mengetikkan-anotasi fungsi Anda.

Analisis tipe tidak berarti banyak.

Agda dikenal memiliki sistem tipe Turing-complete, sangat berbeda (dan jauh lebih sulit untuk dihitung) daripada bahasa ML (misalnya Ocaml ).