DSpec2Test: Pembuatan Tes Berbasis Spesifikasi di Dafny

Pendekatan blackbox berbasis DNF yang mengungguli pembuatan tes berbasis implementasi

Sofia Vieira Pinto; Álvaro F. Silva; João Pascoal Faria; Alexandra Mendes· 2026· DOI 10.48550/arXiv.2609.29713

Masalah inti

Bahasa yang sadar verifikasi seperti Dafny mengintegrasikan konstruksi logika langsung ke dalam kode, memungkinkan verifikasi otomatis atas kebenaran program. Namun, tes tetap bernilai dalam skenario yang tidak ditangani verifikasi saja, seperti mendukung pengembangan berbasis tes. Alat pembuatan tes Dafny yang ada berbasis implementasi, yang membatasi penerapannya ketika spesifikasi menjadi artefak utama. Penulis menyajikan DSpec2Test, alat pembuatan tes berbasis spesifikasi untuk Dafny yang secara otomatis menurunkan tes dari spesifikasi formal tanpa mempertimbangkan detail implementasi. Alat ini memperluas perintah `generate-tests` Dafny dengan mode blackbox baru berdasarkan partisi kelas ekuivalen Disjunctive Normal Form (DNF) dan Boundary Value Analysis (BVA) opsional. DSpec2Test mengandalkan pemecah SMT Z3 untuk menyintesis input dan output yang diharapkan yang memenuhi batasan turunan spesifikasi. Evaluasi menggunakan program dari DafnyBench yang dimutasi dengan MutDafny dan membandingkan DSpec2Test dengan mode Block berbasis implementasi Dafny yang ada.

Evaluasi membandingkan DSpec2Test dengan mode Block berbasis implementasi Dafny yang ada pada dataset 131 mutan yang dihasilkan dari program DafnyBench menggunakan MutDafny. Metrik utamanya adalah tingkat pembunuhan mutasi. DSpec2Test mencapai tingkat pembunuhan mutasi 93,9%, sedangkan Block mencapai 82,4%. Yang patut dicatat, DSpec2Test secara unik membunuh 17 mutan yang tidak dibunuh Block, menunjukkan sifat komplementernya. Hasilnya dirangkum dalam tabel di bawah ini: | Tool | Mutation Kill Rate | |------|-------------------| | DSpec2Test | 93.9% | | Block | 82.4% | Hasil ini menunjukkan bahwa pengujian berbasis spesifikasi adalah pendekatan yang efektif dan komplementer untuk menguji program Dafny. Tingkat pembunuhan yang lebih tinggi menunjukkan bahwa menurunkan tes dari spesifikasi dapat mengungkap kesalahan yang terlewat oleh pengujian berbasis implementasi, terutama ketika implementasi menyimpang dari spesifikasi.

Bahasa yang sadar verifikasi seperti Dafny mengintegrasikan konstruksi logika langsung ke dalam kode, memungkinkan verifikasi otomatis atas kebenaran program. Namun, tes tetap bernilai dalam skenario yang tidak ditangani verifikasi saja, seperti mendukung pengembangan berbasis tes. Alat pembuatan tes Dafny yang ada berbasis implementasi, yang membatasi penerapannya ketika spesifikasi menjadi artefak utama. Penulis menyajikan DSpec2Test, alat pembuatan tes berbasis spesifikasi untuk Dafny yang secara otomatis menurunkan tes dari spesifikasi formal tanpa mempertimbangkan detail implementasi. Alat ini memperluas perintah `generate-tests` Dafny dengan mode blackbox baru berdasarkan partisi kelas ekuivalen Disjunctive Normal Form (DNF) dan Boundary Value Analysis (BVA) opsional. DSpec2Test mengandalkan pemecah SMT Z3 untuk menyintesis input dan output yang diharapkan yang memenuhi batasan turunan spesifikasi. Evaluasi menggunakan program dari DafnyBench yang dimutasi dengan MutDafny dan membandingkan DSpec2Test dengan mode Block berbasis implementasi Dafny yang ada.

DSpec2Test beroperasi sebagai pembuat tes blackbox: ia mengambil spesifikasi Dafny (prasyarat, pascasyarat, dan invarian) dan mengabaikan badan implementasi. Algoritma inti mempartisi ruang input menggunakan partisi kelas ekuivalen DNF. Diberikan spesifikasi, alat mengekstrak batasan logika dan mengonversinya menjadi DNF, di mana setiap disjungsi merepresentasikan kelas ekuivalen input yang berbeda yang memenuhi cabang spesifikasi yang sama. Untuk setiap kelas, Z3 ditanyakan untuk menyintesis nilai input konkret dan output yang diharapkan yang sesuai yang memenuhi pascasyarat. Secara opsional, Boundary Value Analysis (BVA) diterapkan untuk menghasilkan tes tambahan pada batas setiap kelas ekuivalen, meningkatkan deteksi kesalahan untuk kesalahan off-by-one dan kasus tepi. Tes yang dihasilkan dinyatakan sebagai metode tes Dafny yang dapat dijalankan dengan test runner Dafny. Alat ini diimplementasikan sebagai ekstensi perintah `generate-tests` Dafny, menambahkan mode `--blackbox`. Alur kerja diilustrasikan di bawah ini:

Temuan ini menyoroti nilai pembuatan tes berbasis spesifikasi dalam bahasa yang sadar verifikasi. Dengan berfokus pada spesifikasi daripada implementasi, DSpec2Test mendukung pengembangan berbasis tes dan dapat digunakan bahkan sebelum implementasi ada. Penggunaan partisi kelas ekuivalen DNF memastikan cakupan sistematis cabang spesifikasi, sementara BVA opsional menargetkan kondisi batas. Ketergantungan pada Z3 memungkinkan sintesis input dan output yang diharapkan secara tepat. Tingkat pembunuhan mutasi 93,9% dan pembunuhan unik 17 mutan menegaskan peran komplementer pengujian berbasis spesifikasi bersama pendekatan berbasis implementasi. Namun, pendekatan ini mungkin dibatasi oleh kompleksitas spesifikasi dan skalabilitas pemecahan SMT. Pekerjaan selanjutnya dapat mengeksplorasi penggabungan kedua mode, memperluas ke bahasa sadar verifikasi lain, dan mengintegrasikan dengan pipeline integrasi berkelanjutan. Secara keseluruhan, DSpec2Test merepresentasikan langkah signifikan menuju pengujian yang lebih efektif di lingkungan pengembangan formal.

Praktisi dan peneliti ilmu komputer

Membuka konten member…