NASALib adalah upaya kolaboratif berkelanjutan yang telah berlangsung selama lebih dari 3 dekade, untuk membantu penelitian terkait pembuktian teorema yang disponsori oleh NASA (https://shemesh.larc.nasa.gov/fm/pvs/). Ini terdiri dari kumpulan pengembangan formal (yaitu perpustakaan ) yang ditulis dalam Sistem Verifikasi Prototipe (PVS), disumbangkan oleh SRI, NASA, NIA, dan komunitas PVS, dan dikelola oleh Tim Metode Formal di LaRC.
Versi NASALib saat ini adalah 7.1.2 (2023/09/01) dan membutuhkan PVS 7.1.
Saat ini, NASALib terdiri dari 62 perpustakaan tingkat atas , berisi total sekitar 38 ribu formula yang telah terbukti.
| Perpustakaan | Keterangan |
|---|---|
| Sesuai | Kerangka analisis algoritma deteksi dan resolusi konflik lalu lintas udara |
| affine_arith | Formalisasi aritmatika affine dan strategi evaluasi fungsi polinomial dengan variabel pada domain interval |
| aljabar | Grup, monoid, cincin, dll |
| analisa | Analisis real, limit, kontinuitas, turunan, integral |
| ASP | Semantik denotasi Pemrograman Kumpulan Jawaban |
| penerbangan | Mendukung definisi dan properti untuk formalisasi terkait penerbangan |
| Bernstein | Formalisasi polinomial Bernstein multivariat |
| CCG | Formalisasi kriteria penghentian yang beragam |
| kompleks | Bilangan kompleks |
| kompleks_alt | Formalisasi alternatif bilangan kompleks |
| kompleks_integrasi | Integrasi yang kompleks |
| struktur_sama | Urutan panjang yang dapat dihitung didefinisikan sebagai tipe data ko-aljabar |
| digraf | Grafik berarah: sirkuit, subpohon maksimal, jalur, DAG |
| dL | Logika Dinamis Diferensial |
| tepat_nyata_arith | Aritmatika nyata yang tepat termasuk fungsi trigonometri |
| contoh | Contoh penerapan fungsi yang disediakan oleh NASALib |
| diperpanjang_nnreal | Real non-negatif yang diperluas |
| cepat_kira-kira | Perkiraan fungsi numerik standar |
| kesalahan_toleransi | Protokol toleransi kesalahan |
| mengambang | Aritmatika titik mengambang |
| grafik | Teori grafik |
| interval_arith | Aritmatika interval dan perkiraan numerik. Mencakup strategi numerik otomatis untuk menghitung perkiraan numerik dan interval untuk memeriksa kepuasan dan validitas rumus nilai riil yang dikuantifikasi secara sederhana. Perkembangan ini mencakup formalisasi logika temporal interval Allen |
| int | Pembagian bilangan bulat, gcd, mod, faktorisasi prima, min, maks |
| lebesgue | Integral Lebesgue dengan koneksi ke Integral Riemann |
| linear_aljabar | Aljabar linier |
| baris_segmen | Segmen garis 2 dimensi |
| dalam pengalaman | Logaritma, fungsi eksponensial dan hiperbolik. & Definisi dasar fungsi logaritma, eksponensial dan hiperbolik |
| LTL | Logika Temporal Linier |
| matriks | Spesifikasi matriks MxN yang dapat dieksekusi. Pustaka ini mencakup perhitungan operasi invers dan matriks dasar seperti penjumlahan dan perkalian |
| ukuran_integrasi | Aljabar Sigma, ukuran, Fubini-Tonelli Lemmas |
| MetiTarski | Integrasi MetiTarski, pembukti teorema otomatis untuk fungsi bernilai nyata |
| ruang_metrik | Domain dengan metrik jarak, kontinuitas, dan kontinuitas seragam |
| mv_analisis | Analisis nyata multivariat: norma, batasan, kontinuitas, turunan, optimasi, dll. |
| multi_poli | Polinomial multivariat dan himpunan semi-aljabar. |
| nominal | Penalaran persamaan nominal |
| angka | Teori bilangan dasar |
| ODE | Persamaan Diferensial Biasa |
| pesanan | Perintah abstrak, kisi, titik perbaikan |
| poligon | poligon 2 dimensi |
| poligon_merge | Gabungkan poligon 2 dimensi tanpa menghasilkan lubang |
| kekuatan | Fungsi Daya Umum (tanpa ln/exp) |
| kemungkinan | Teori probabilitas |
| PVS0 | Formalisasi konsep dasar komputasi |
| pvsio_utils | Penambahan pada PVSio, pustaka standar PVS untuk animasi spesifikasi PVS |
| nyata | Penjumlahan, sup, inf, sqrt atas real, nilai absolut, dll |
| Riemann | Integral Riemann |
| scott | Topologi Scott |
| seri | Deret pangkat, uji perbandingan, uji rasio, teorema Taylor |
| set_aux | Himpunan pangkat, tatanan, kardinalitas terhadap himpunan tak terhingga. Mencakup fakta fungsional dan relasional berdasarkan Aksioma Pilihan dan penyempurnaan hubungan berdasarkan hubungan kesetaraan |
| bentuk | Bentuk 2D: segitiga, jajar genjang, persegi panjang, ruas lingkaran |
| sigma_set | Penjumlahan atas himpunan tak terhingga |
| penyortiran | Algoritma pengurutan |
| struktur | Array berbatas, barisan berhingga, kantong, dan beberapa struktur lainnya |
| Badai | Formalisasi teorema Sturm untuk polinomial univariat. Termasuk strategi sturm dan mono-poly untuk secara otomatis membuktikan hubungan polinomial univariat dalam interval nyata |
| Tarski | Formalisasi teorema Tarski untuk polinomial univariat. Termasuk strategi tarski untuk secara otomatis membuktikan sistem hubungan polinomial univariat pada garis nyata |
| topologi | Kontinuitas, homeomorfisme, ruang terhubung dan kompak, himpunan/fungsi Borel |
| trigonometri | Trigonometri: definisi, identitas, perkiraan |
| TRS | Istilah sistem penulisan ulang dan algoritma penyatuan Robinson |
| TU_permainan | Permainan TU kooperatif |
| vect_analisis | Limit, kontinuitas, dan turunan fungsi vektor |
| vektor | Vektor 2-D, 3-D, 4-D, dan n-dimensi |
| ketika | Semantik untuk bahasa pemrograman While |
NASALib juga menyediakan kumpulan skrip yang mengotomatiskan beberapa tugas.
proveit (*) - Menjalankan PVS dalam mode batchprovethem (*) - Menjalankan proveit di beberapa perpustakaanpvsio (*) - Utilitas baris perintah untuk menjalankan evaluator lapangan PVSio.prove-all - Menjalankan proveit di setiap perpustakaan di NASALib dengan membungkus provethem untuk menyediakan jenis proses tertentu.cleanbin-all - Bersihkan file .pvscontext dan biner dari perpustakaan PVS.find-all - Mencari string yang cocok dengan ekspresi reguler tertentu di perpustakaan PVS.dependencygraph - Menghasilkan grafik ketergantungan perpustakaan untuk perpustakaan di direktori saat ini.dependency-all - Menghasilkan grafik ketergantungan untuk perpustakaan PVS di folder saat ini.Klik di sini untuk rincian lebih lanjut tentang skrip ini.
(*) Sudah termasuk dalam distribusi PVS 7.1.
NASALib (v7.0.1) sepenuhnya kompatibel dengan VSCode-PVS, antarmuka grafis modern untuk PVS berdasarkan Visual Studio Code. Versi terbaru NASALib dapat diinstal dari VSCode-PVS.
Untuk pengguna tingkat lanjut PVS, versi pengembangan tersedia dari GitHub. Untuk mengkloning versi pengembangan, ketikkan perintah berikut di dalam direktori tempat PVS 7.0 diinstal. Selanjutnya, direktori tersebut akan disebut sebagai
$ git clone http://github.com/nasa/pvslib nasalib Perintah di atas akan meletakkan salinan perpustakaan di direktori
groups perpustakaan sekarang tidak digunakan lagi . Perpustakaan group diintegrasikan ke dalam algebra . Tautan simbolik masih disediakan untuk kompatibilitas ke belakang, namun penggunaannya tidak disarankan. Setiap penyebutan groups harus diganti dengan algebra .
Perpustakaan trig_fnd sekarang tidak digunakan lagi . Itu masih disediakan untuk kompatibilitas ke belakang, tetapi harus diganti dengan trig . trig perpustakaan baru, yang dulunya bersifat aksiomatik, kini menjadi dasar. Namun, berbeda dengan trig_fnd , definisi trigonometri didasarkan pada deret tak hingga, bukan integral. Perubahan ini sangat mengurangi pengecekan tipe pada teori yang melibatkan fungsi trigonometri. Perubahan dari trig_fnd ke trig seharusnya tidak berdampak besar pada perkembangan formal Anda karena nama definisi dan lemmanya sama. Namun, pengimporan teori mungkin sedikit berbeda.
Pengembangan PVS TCASII , WellClear , dan DAIDALUS kini tersedia sebagai bagian dari distribusi GitHub WellClear. PRECiSA pengembangan PVS sekarang tersedia sebagai bagian dari distribusi GitHub PRECiSA. PolyCARP pengembangan PVS sekarang tersedia sebagai bagian dari distribusi GitHub PolyCARP.
Petunjuk berikut mengasumsikan bahwa NASALib terletak di direktori
PVS_LIBRARY_PATH Jika tidak ada, buat variabel tersebut dan dengan jalur direktori ini hanya sebagai konten. Biasanya akan sangat berguna jika sistem shell Anda membuat variabel ini saat startup. Untuk tujuan ini, dan bergantung pada shell Anda, Anda mungkin ingin menambahkan salah satu baris berikut di skrip startup Anda. Untuk C shell (csh atau tcsh), Anda dapat menambahkan baris ini di ~/.cshrc :
setenv PVS_LIBRARY_PATH " /nasalib " Untuk Borne shell (bash atau sh), tambahkan baris ini di ~/.bashrc atau ~/.profile :
export PVS_LIBRARY_PATH= " /nasalib " Jika Anda memiliki instalasi NASALib sebelumnya, hapus file ~/.pvs.lisp atau, jika Anda memiliki konfigurasi khusus di file itu, hapus baris berikut
( load " /nasalib/pvs-patches.lisp " ) Terakhir, buka direktori
Perintah install-scripts akan memperbarui dan menginstal skrip NASALib sesuai kebutuhan.
$ ./install-scriptsVersi NASALib yang lebih lama tersedia di http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library.
NASALib telah berkembang selama bertahun-tahun berkat kontribusi beberapa orang, di antaranya:
Jika kami salah mengatribusikan pengembangan PVS atau Anda telah berkontribusi pada NASALib dan nama Anda tidak disertakan di sini, harap beri tahu kami.
Jika Anda ingin berkontribusi silakan baca panduan ini.
NASALib adalah kumpulan spesifikasi formal yang sebagian besar telah berada dalam domain publik selama beberapa tahun. Tim Metode Formal di NASA LaRC masih mempertahankan perkembangan tersebut. Untuk pengembangan yang semula dilakukan oleh Tim Metode Formal, pengembangan tersebut dianggap sebagai penelitian mendasar yang bukan merupakan perangkat lunak. Kontribusi yang dibuat oleh orang lain mungkin memiliki lisensi tertentu, yang tercantum dalam file top.pvs di masing-masing direktori. Jika ragu, silakan hubungi pengembang masing-masing kontribusi, yang juga tercantum dalam file tersebut.
Patch PVS, yang termasuk dalam direktori pvs-patches , adalah bagian dari kode sumber PVS dan dilindungi oleh lisensi sumber terbuka PVS.
Beberapa strategi pembuktian memerlukan alat penelitian pihak ketiga, misalnya MetiTarski dan Z3. Untuk kenyamanan, mereka disertakan dalam repositori ini dengan izin dari penulisnya. Lisensi untuk alat-alat ini juga disertakan jika diperlukan.
Nikmatilah.
Tim Metode Formal di LaRC
Cesar Muñoz Mariano Moscato
