anthem 1

lagu kebangsaan

Terjemahkan program kumpulan jawaban ke bahasa pembukti teorema orde pertama

Status proyek ini

Catatan

Saat ini Anda sedang melihat anthem versi 1, yang dibuat oleh Patrick Lühne dan tidak lagi dikembangkan. Tidak ada komitmen lebih lanjut terhadap repositori ini yang akan dilakukan.

Jika Anda tertarik dengan lagu versi terbaru, lihat repositori baru.

Ringkasan

anthem menerjemahkan program ASP (dalam bahasa input clingo ) ke bahasa pembukti teorema orde pertama seperti Prover9.

Penggunaan

Untuk memverifikasi bahwa suatu program mengimplementasikan suatu spesifikasi, aktifkan anthem menggunakan perintah verify-program :

 $ lagu verifikasi-program  ...

Perhatikan bahwa beberapa file spesifikasi mungkin ditentukan. Hal ini berguna untuk memisahkan lemma dan aksioma dari asumsi dan spesifikasi.

Contoh penghitungan dasar akar kuadrat suatu bilangan dapat direproduksi sebagai berikut:

 $ lagu verifikasi-contoh program/contoh-2.{lp,spec,lemmas}

Notasi kurung kurawal adalah singkatan dari Bash

 $ lagu verifikasi-contoh program/contoh-2.lp contoh/contoh-2.spec contoh/contoh-2.lemmas

Secara default, anthem melakukan penyelesaian Clark pada rumus yang diterjemahkan, mendeteksi variabel mana yang bilangan bulat, dan menyederhanakan keluaran dengan menerapkan beberapa aturan transformasi dasar.

Langkah-langkah pemrosesan ini dapat dimatikan dengan opsi --no-complete , --no-simplify , dan --no-detect-integers .

Bangunan

anthem dibuat dengan rantai cargo Rust. Setelah menginstal Rust, anthem dapat dibuat sebagai berikut:

 $ git klon https://github.com/potassco/anthem.git
$ cd lagu kebangsaan
$ pembuatan kargo --rilis

Biner anthem kemudian akan tersedia di direktori target/release/ . Alternatifnya, anthem dapat dipanggil menggunakan cargo sebagai berikut:

 $ kargo dijalankan -- verifikasi-program  ...

Kontributor

• Patrick Luhne