Tangkap kucing dengan TLA +

Metode formal dianggap sebagai cara yang efektif, tetapi tidak rumit untuk memastikan keandalan perangkat lunak. Alat yang digunakan untuk ini berbeda secara signifikan dari yang akrab dengan programmer. Artikel ini ditulis dengan tujuan menurunkan ambang untuk memasuki toolkit ini. Saya akan menggunakan sistem pengecekan model untuk tidak menyelesaikan tugas-tugas yang sulit dirumuskan dari spesifikasi perangkat lunak, tetapi untuk memecahkan teka-teki yang dapat dimengerti bahkan untuk anak sekolah.

Anda berada di koridor langsung dengan tujuh kamar di satu sisi. Salah satunya adalah kucing. Dalam satu langkah, Anda bisa melihat ke salah satu kamar, jika ada kucing, dia tertangkap. Segera setelah pintu ditutup, kucing akan pindah ke salah satu kamar di sebelahnya. Tugasnya adalah menangkap kucing.

TLA + dan logika temporal

Ada banyak alat yang dapat memecahkan masalah seperti itu. Seringkali dalam kasus seperti itu, solver SMT digunakan. Sebagai aturan, sistem seperti itu menggunakan logika predikat biasa dan mengekspresikan urutan tindakan cukup rumit (Anda harus menggunakan sesuatu seperti array, yang sangat tidak nyaman untuk digunakan). TLA + menggunakan logika temporal, yang memungkinkan penggunaan status sistem dalam satu pernyataan baik pada saat ini dan pada langkah berikutnya.

CatDistr' = CatDistr \ {n} 

Kondisi ini menyatakan bahwa set kamar tempat kucing dapat ditemukan setelah memeriksa kamar n bertepatan dengan set kamar tempat n diambil (jika kucing ada di sana, ia ditangkap dan tidak ada lagi yang harus dilakukan).

Dalam bahasa pemrograman imperatif, ini kira-kira sama dengan menugaskan variabel nilai baru, dihitung dari yang lama.

Sedikit tentang set

Seperti yang Anda pahami, posisi kucing dimodelkan oleh variabel dengan himpunan semua kamar yang mungkin, dan bukan kamar tertentu, karena akan berada dalam sistem simulasi. Menggunakan himpunan nilai yang mungkin sebagai ganti nilai tertentu adalah teknik yang sering digunakan dalam metode formal, yang menyebabkan kesulitan bagi programmer pemula. Oleh karena itu, saya memilih tugas yang penggunaan setnya sesuai.

Struktur Program dalam TLA +

Dalam kasus yang paling sederhana, program terdiri dari deklarasi dan pernyataan (predikat) yang menggambarkan keadaan awal, hubungan antara kondisi saat ini dan selanjutnya, dan invarian yang harus dieksekusi di semua negara yang tersedia. Predikat tambahan juga mungkin ada. Predikat dapat diparameterisasi.

 ---- MODULE cat ------------------------------------------------------------- EXTENDS Integers CONSTANTS Doors VARIABLES CatDistr, LastDoor Init == /\ CatDistr = 0..Doors /\ LastDoor = -1 OpenDoor(n) == /\ CatDistr' = 0..Doors \intersect UNION { {x-1, x+1} : x \in CatDistr \ {n} } /\ LastDoor' = n Next == \E door \in 0..Doors : OpenDoor(door) CatWalk == CatDistr /= {} ============================================================================= 

Baris pertama dan terakhir adalah fitur sintaks dari deklarasi modul.

== berarti "sama dengan definisi", sedangkan satu = adalah persamaan dari nilai-nilai ekspresi yang dihitung.

Pintu adalah model konstan, harus diatur dalam file konfigurasi.
CatDistr - distribusi kucing di kamar.

Variabel LastDoor, ruang terakhir diperiksa, dimasukkan untuk keterbacaan hasil program. Untuk model besar, variabel tersebut dapat secara signifikan memperlambat program dengan meningkatkan jumlah negara yang dianalisis (karena negara sekarang berisi sejarah bagaimana itu muncul dan negara yang sama yang dibuat dengan cara yang berbeda sekarang akan berbeda).

Predikat Init menggambarkan keadaan awal (0..Doors adalah himpunan semua kamar). OpenDoor (n) menggambarkan apa yang terjadi ketika Anda membuka pintu ke kamar n (dalam kasus terburuk, kucing tidak ada di sana - jika tidak kami menangkapnya).

Predikat Next terlihat sedikit aneh - ada ruang untuk melihatnya. Faktanya adalah bahwa keberadaan sesuatu berarti bahwa TLA + tidak tahu ruangan mana yang akan kita lihat, oleh karena itu, itu akan memeriksa kebenaran invarian dalam semua kasus.

Akan lebih jelas untuk menulis

 Next == OpenDoor(0) \/ OpenDoor(1) \/ ... \/ OpenDoor(Doors) 

tapi kemudian kode kita hanya akan berfungsi dengan jumlah kamar yang tetap, dan lebih baik membuatnya parameter.

Akhirnya, invarian CatWalk adalah banyak kamar di mana kucing mungkin tidak kosong. Pelanggaran terhadap invarian berarti kucing itu ditangkap, di mana pun asalnya. Saat memverifikasi spesifikasi, pelanggaran terhadap invarian berarti kesalahan, tetapi kami tidak menggunakan alat untuk tujuan yang dimaksud dan "kesalahan" yang ditemukan berarti menyelesaikan masalah.

Konfigurasi model

 CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk 

Semuanya sederhana di sini - kami menunjukkan jumlah kamar, kondisi awal, kondisi untuk perubahan keadaan, dan invarian yang sedang diuji.

Model diluncurkan dari baris perintah tlc2 -config cat.cfg cat.tla .

TLA + memiliki GUI canggih yang diluncurkan oleh tim tla-toolbox. Sayangnya, ia tidak mengerti file .cfg dan parameter model perlu dikonfigurasi melalui menu.

Kesimpulan

Dalam tugas ini, semuanya ternyata cukup sederhana. Tentu saja, kasus-kasus praktis yang signifikan dalam penerapan metode formal akan memerlukan model yang jauh lebih banyak dan penggunaan berbagai konstruksi bahasa. Tapi saya berharap memecahkan teka-teki seperti itu akan memberikan cara yang sederhana dan tidak membosankan untuk memperkenalkan metode formal dalam proyek kerja.

→ Tugas ditemukan di sini

Untuk jaga-jaga, program sederhana untuk verifikasi solusi interaktif . Bahan untuk studi TLA + . Sistem pengecekan model lain, Alloy, dijelaskan di sini .