Mengapa kita tidak meneliti lebih lanjut tentang menyusun jaminan waktu?

Saya suka semua itu waktu kompilasi dan saya suka ide bahwa setelah Anda menyusun program banyak jaminan dibuat tentang eksekusi itu. Secara umum sistem tipe statis (Haskell, C ++, ...) tampaknya memberikan jaminan waktu kompilasi yang lebih kuat daripada sistem tipe dinamis apa pun.

Dari apa yang saya pahami, Ada melangkah lebih jauh dalam hal mengkompilasi pengecekan waktu, dan mampu mendeteksi sejumlah bug yang lebih besar sebelum eksekusi. Itu juga dianggap cukup aman, mengingat bahwa, pada suatu titik waktu, itu dipilih untuk bidang yang rumit (ketika kesalahan pemrograman mungkin menelan korban jiwa manusia).

Sekarang, saya bertanya-tanya: jika jaminan statis yang lebih kuat, mengarah ke kode yang lebih terdokumentasi dan aman, mengapa kita tidak meneliti lebih lanjut ke arah itu?

Contoh dari sesuatu yang tampaknya hilang, akan menjadi bahasa yang alih-alih mendefinisikan inttipe generik yang memiliki rentang yang ditentukan oleh jumlah bit arsitektur yang mendasarinya, seseorang dapat memiliki rentang (dalam contoh berikut ini Int [a..b]menjelaskan jenis integer antara a dan b termasuk):

a : Int [1..24]
b : Int [1..12]
a + b : Int [2..36]
a - b : Int [-11..23]
b - a : Int [-23..11]

atau (mengambil ini dari Ada):

a : Int [mod 24]
b : Int [mod 24]
a + b : Int [mod 24]

Bahasa ini akan memilih jenis yang mendasari terbaik untuk rentang dan akan melakukan kompilasi waktu memeriksa ekspresi. Jadi, misalnya, diberikan:

a : Int [-3..24]
b : Int [3..10]

kemudian:

a / b

tidak akan pernah tidak didefinisikan.

Ini hanya sebuah contoh tapi saya merasa ada banyak lagi yang bisa kita terapkan pada waktu kompilasi. Jadi, mengapa ada sedikit penelitian tentang ini? Apa istilah teknis yang menggambarkan ide ini (sehingga saya dapat menemukan lebih banyak informasi tentang topik ini)? Apa batasannya?

Saya tidak dalam posisi untuk mengatakan berapa banyak lebih penelitian harus dilakukan pada topik, tapi saya dapat memberitahu Anda bahwa ada adalah penelitian yang dilakukan, misalnya Verisoft XT program yang didanai oleh pemerintah Jerman.

Konsep yang saya pikir Anda cari disebut verifikasi formal dan pemrograman berbasis kontrak , di mana yang terakhir adalah cara yang ramah programmer untuk melakukan yang pertama. Dalam pemrograman berbasis kontrak Anda pertama-tama menulis kode Anda seperti biasa dan kemudian memasukkan apa yang disebut kontrak ke dalam kode. Bahasa yang mudah digunakan yang didasarkan pada paradigma ini adalah Spec # oleh Microsoft Research, dan ekstensi Kontrak Kode yang secara fungsional serupa tetapi sedikit kurang cantik untuk C # yang bisa Anda coba secara online (mereka juga memiliki alat serupa untuk bahasa lain, lihat rise4fun ). "Int with range type" yang Anda sebutkan akan tercermin oleh dua kontrak dalam suatu fungsi:

Contract.Requires(-3 <= a && a <= 24);
Contract.Requires( 3 <= b && b <= 10);

Jika Anda ingin memanggil fungsi itu, Anda harus menggunakan parameter yang dipastikan memenuhi kriteria ini, atau Anda mendapatkan kesalahan waktu kompilasi. Di atas adalah kontrak yang sangat sederhana, Anda dapat memasukkan hampir semua asumsi atau persyaratan tentang variabel atau pengecualian dan hubungan mereka yang mungkin Anda pikirkan dan kompiler akan memeriksa apakah setiap persyaratan dicakup oleh asumsi atau sesuatu yang dapat dipastikan, yaitu berasal dari asumsi. Itulah sebabnya dari mana nama itu berasal: Callee membuat persyaratan , penelepon memastikan bahwa ini dipenuhi - seperti dalam kontrak bisnis.

$P(x_1,x_2,...,x_n)$$n$$P$digunakan. Dari sisi CS, keduanya adalah bagian penting dari proses - pembuatan kondisi verifikasi rumit dan SMT merupakan masalah NP-complete atau tidak dapat diputuskan, tergantung pada teori yang dipertimbangkan. Bahkan ada kompetisi untuk pemecah SMT, jadi pasti ada beberapa penelitian tentang ini. Selain itu, ada pendekatan alternatif untuk menggunakan SMT untuk verifikasi formal seperti penghitungan ruang negara, pengecekan model simbolis, pengecekan model terikat dan banyak lagi yang sedang diteliti, walaupun SMT, afaik, saat ini merupakan pendekatan yang paling "modern".

Mengenai batasan gagasan umum:

• Seperti yang dinyatakan sebelumnya, membuktikan kebenaran program adalah masalah yang sulit secara komputasi, sehingga mungkin saja pemeriksaan waktu kompilasi suatu program dengan kontrak (atau bentuk spesifikasi lainnya) memakan waktu sangat lama atau bahkan mungkin mustahil. Menerapkan heuristik yang berfungsi dengan baik sebagian besar waktu adalah yang terbaik yang bisa dilakukan tentang hal itu.
• Semakin banyak Anda menentukan tentang program Anda, semakin tinggi kemungkinan memiliki bug dalam spesifikasi itu sendiri . Hal ini dapat mengarah pada false positive (pemeriksaan waktu kompilasi gagal meskipun semuanya bebas bug) atau kesan salah karena aman, meskipun program Anda masih memiliki bug.
• Menulis kontrak atau spesifikasi adalah pekerjaan yang sangat membosankan dan kebanyakan programmer terlalu malas untuk melakukannya. Cobalah menulis program C # dengan kontrak kode di mana-mana, setelah beberapa saat Anda akan berpikir "ayolah, apakah ini benar-benar diperlukan?". Itulah sebabnya verifikasi formal biasanya hanya digunakan untuk desain perangkat keras dan sistem kritis keselamatan, seperti perangkat lunak yang mengendalikan pesawat terbang atau otomotif.

Satu hal terakhir yang layak disebutkan yang tidak cukup cocok dengan penjelasan di atas adalah bidang yang disebut "Teori Kompleksitas Implisit", misalnya tulisan ini . Ini bertujuan untuk mengkarakterisasi bahasa pemrograman di mana setiap program yang Anda dapat tulis termasuk dalam kelas kompleksitas tertentu, misalnya P. Dalam bahasa seperti itu, setiap program yang Anda tulis secara otomatis "dipastikan" memiliki runtime polinomial, yang dapat "diperiksa" pada waktu kompilasi dengan hanya menyusun program. Namun, saya tidak tahu hasil praktis apa pun yang dapat digunakan dari penelitian ini, tetapi saya juga jauh dari ahli.