NASALib เป็นความพยายามในการทำงานร่วมกันอย่างต่อเนื่องที่มีระยะเวลากว่า 3 ทศวรรษ เพื่อช่วยในการวิจัยที่เกี่ยวข้องกับทฤษฎีบทที่ได้รับการพิสูจน์โดย NASA (https://shemesh.larc.nasa.gov/fm/pvs/) ประกอบด้วยชุดของการพัฒนาอย่างเป็นทางการ (เช่น ห้องสมุด ) ที่เขียนในระบบการตรวจสอบต้นแบบ (PVS) ซึ่งสนับสนุนโดย SRI, NASA, NIA และชุมชน PVS และดูแลโดยทีมวิธีการอย่างเป็นทางการที่ LaRC
NASALib เวอร์ชันปัจจุบันคือ 7.1.2 (2023/09/01) และต้องใช้ PVS 7.1
ปัจจุบัน NASALib ประกอบด้วยห้องสมุด ระดับบนสุด 62 แห่ง ซึ่งมีสูตรที่ได้รับการพิสูจน์แล้วทั้งหมดประมาณ 38,000 สูตร
| ห้องสมุด | คำอธิบาย |
|---|---|
| แอคคอร์ด | กรอบการทำงานสำหรับการวิเคราะห์อัลกอริธึมการตรวจจับข้อขัดแย้งของการจราจรทางอากาศและการแก้ไข |
| affine_arith | การทำเลขคณิตและกลยุทธ์แบบแอฟฟีนอย่างเป็นทางการสำหรับการประเมินฟังก์ชันพหุนามที่มีตัวแปรบนโดเมนช่วง |
| พีชคณิต | หมู่ โมโนอยด์ วงแหวน ฯลฯ |
| การวิเคราะห์ | การวิเคราะห์จริง ขีดจำกัด ความต่อเนื่อง อนุพันธ์ ปริพันธ์ |
| งูเห่า | ความหมายเชิง Denotational ของการเขียนโปรแกรมชุดคำตอบ |
| การบิน | สนับสนุนคำจำกัดความและคุณสมบัติสำหรับพิธีการที่เกี่ยวข้องกับการบิน |
| เบิร์นสไตน์ | การทำให้เป็นทางการของพหุนามเบิร์นสไตน์หลายตัวแปร |
| ซีซีจี | การกำหนดเกณฑ์การเลิกจ้างที่หลากหลายอย่างเป็นทางการ |
| ซับซ้อน | จำนวนเชิงซ้อน |
| complex_alt | การทำรูปแบบทางเลือกของจำนวนเชิงซ้อน |
| complex_integration | บูรณาการที่ซับซ้อน |
| โครงสร้างร่วม | ลำดับของความยาวที่นับได้ซึ่งกำหนดเป็นประเภทข้อมูลพีชคณิตร่วม |
| ไดกราฟ | กราฟกำกับ: วงจร, แผนผังย่อยสูงสุด, เส้นทาง, DAG |
| เดซิลิตร | ลอจิกไดนามิกดิฟเฟอเรนเชียล |
| แน่นอน_real_arith | เลขคณิตจริงที่แน่นอนรวมทั้งฟังก์ชันตรีโกณมิติ |
| ตัวอย่าง | ตัวอย่างการใช้งานฟังก์ชันที่จัดทำโดย NASALib |
| Extended_nnreal | ขยายจำนวนจริงที่ไม่เป็นลบ |
| รวดเร็ว_ประมาณ | การประมาณฟังก์ชันตัวเลขมาตรฐาน |
| ความผิดพลาด_ความอดทน | โปรโตคอลการยอมรับข้อผิดพลาด |
| ลอย | เลขคณิตจุดลอยตัว |
| กราฟ | ทฤษฎีกราฟ |
| ช่วง_arith | เลขคณิตช่วงและการประมาณตัวเลข รวมกลยุทธ์อัตโนมัติเชิงตัวเลขสำหรับการคำนวณการประมาณเชิงตัวเลขและช่วงเวลาสำหรับการตรวจสอบความพึงพอใจและความถูกต้องของสูตรมูลค่าจริงเชิงปริมาณ การพัฒนานี้รวมถึงการปรับลอจิกขมับช่วงอัลเลนอย่างเป็นทางการ |
| int | การหารจำนวนเต็ม gcd mod การแยกตัวประกอบเฉพาะ ค่าต่ำสุด ค่าสูงสุด |
| เลเบสเกอ | Lebesgue บูรณาการกับการเชื่อมต่อกับ Riemann Integral |
| linear_algebra | พีชคณิตเชิงเส้น |
| line_segments | ส่วนของเส้นตรง 2 มิติ |
| lnexp | ฟังก์ชันลอการิทึม เลขชี้กำลัง และไฮเพอร์โบลิก & คำจำกัดความพื้นฐานของฟังก์ชันลอการิทึม เลขชี้กำลัง และไฮเปอร์โบลิก |
| แอลทีแอล | ลอจิกเวลาเชิงเส้น |
| เมทริกซ์ | ข้อมูลจำเพาะที่ปฏิบัติการได้ของเมทริกซ์ MxN ไลบรารีนี้รวมการคำนวณการดำเนินการเมทริกซ์ผกผันและพื้นฐาน เช่น การบวกและการคูณ |
| การวัด_บูรณาการ | พีชคณิตซิกมา, การวัด, บทแทรก Fubini-Tonelli |
| เมติทาร์สกี้ | การบูรณาการ MetiTarski ซึ่งเป็นเครื่องพิสูจน์ทฤษฎีบทอัตโนมัติสำหรับฟังก์ชันมูลค่าจริง |
| metric_space | โดเมนที่มีการวัดระยะทาง ความต่อเนื่อง และความต่อเนื่องสม่ำเสมอ |
| mv_การวิเคราะห์ | การวิเคราะห์จริงหลายตัวแปร: บรรทัดฐาน ขีดจำกัด ความต่อเนื่อง อนุพันธ์ การเพิ่มประสิทธิภาพ ฯลฯ |
| multi_poly | พหุนามหลายตัวแปรและเซตกึ่งพีชคณิต |
| ระบุ | การใช้เหตุผลสมการที่กำหนด |
| ตัวเลข | ทฤษฎีจำนวนเบื้องต้น |
| ODE | สมการเชิงอนุพันธ์สามัญ |
| คำสั่งซื้อ | คำสั่งนามธรรม โครงตาข่าย จุดแก้ไข |
| รูปหลายเหลี่ยม | รูปหลายเหลี่ยม 2 มิติ |
| รูปหลายเหลี่ยม_ผสาน | ผสานรูปหลายเหลี่ยม 2 มิติโดยไม่สร้างรู |
| พลัง | ฟังก์ชันกำลังทั่วไป (ไม่มี ln/exp) |
| ความน่าจะเป็น | ทฤษฎีความน่าจะเป็น |
| PVS0 | การทำแนวคิดพื้นฐานด้านการคำนวณขั้นพื้นฐานอย่างเป็นทางการ |
| pvsio_utils | ส่วนเพิ่มเติมของ PVSio ซึ่งเป็นไลบรารีมาตรฐาน PVS สำหรับแอนิเมชันของข้อกำหนด PVS |
| ของจริง | ผลรวม, sup, inf, sqrt เหนือจำนวนจริง, ค่าสัมบูรณ์ ฯลฯ |
| รีมันน์ | อินทิกรัลรีมันน์ |
| สกอตต์ | โทโพโลยีสกอตต์ |
| ชุด | อนุกรมกำลัง การทดสอบเปรียบเทียบ การทดสอบอัตราส่วน ทฤษฎีบทของเทย์เลอร์ |
| ชุด_aux | เซตกำลัง ลำดับ จำนวนนับ ส่วนเซตอนันต์ รวมข้อเท็จจริงเชิงฟังก์ชันและเชิงสัมพันธ์ตามสัจพจน์ของตัวเลือก และความสัมพันธ์เชิงปรับแต่งตามความสัมพันธ์ที่เท่าเทียมกัน |
| รูปร่าง | รูปร่าง 2 มิติ: สามเหลี่ยม สี่เหลี่ยมด้านขนาน สี่เหลี่ยม ส่วนวงกลม |
| sigma_set | ผลบวกของเซตอนันต์นับได้ |
| การเรียงลำดับ | อัลกอริธึมการเรียงลำดับ |
| โครงสร้าง | อาร์เรย์ที่มีขอบเขต ลำดับจำกัด ถุง และโครงสร้างอื่นๆ อีกหลายรายการ |
| พายุ | การทำทฤษฎีบทของสตวร์มอย่างเป็นทางการสำหรับพหุนามแบบตัวแปรเดียว รวมกลยุทธ์ sturm และ mono-poly สำหรับการพิสูจน์ความสัมพันธ์พหุนามแบบตัวแปรเดียวโดยอัตโนมัติในช่วงเวลาจริง |
| ทาร์สกี้ | การทำทฤษฎีบทของทาร์สกีอย่างเป็นทางการสำหรับพหุนามแบบตัวแปรเดียว รวมกลยุทธ์ทาร์สกีสำหรับการพิสูจน์ระบบความสัมพันธ์พหุนามแบบตัวแปรเดียวบนเส้นจริงโดยอัตโนมัติ |
| โทโพโลยี | ความต่อเนื่อง โฮมโอมอร์ฟิซึม พื้นที่ที่เชื่อมต่อและกะทัดรัด ชุด/ฟังก์ชันบอเรล |
| หนุน | ตรีโกณมิติ: คำจำกัดความ อัตลักษณ์ การประมาณ |
| ทีอาร์เอส | ระบบการเขียนซ้ำภาคเรียนและอัลกอริธึมการรวมโรบินสัน |
| TU_เกม | เกมสหกรณ์ TU |
| vect_analysis | ขีดจำกัด ความต่อเนื่อง และอนุพันธ์ของฟังก์ชันเวกเตอร์ |
| เวกเตอร์ | เวกเตอร์ 2 มิติ, 3 มิติ, 4 มิติ และ n มิติ |
| ในขณะที่ | ความหมายสำหรับภาษาโปรแกรม While |
NASALib ยังมีคอลเลกชันสคริปต์ที่ทำให้งานหลายอย่างเป็นไปโดยอัตโนมัติ
proveit (*) - รัน PVS ในโหมดแบตช์provethem (*) - เรียก proveit พิสูจน์ในห้องสมุดหลายแห่งpvsio (*) - ยูทิลิตี้บรรทัดคำสั่งเพื่อรันตัวประเมินภาคพื้นดิน PVSioprove-all - รัน proveit ในแต่ละไลบรารีใน NASALib โดยการรวม provethem เพื่อจัดเตรียมการรันประเภทเฉพาะcleanbin-all - ล้างไฟล์ .pvscontext และไบนารี่จากไลบรารี PVSfind-all - ค้นหาสตริงที่ตรงกับนิพจน์ทั่วไปที่กำหนดในไลบรารี PVSdependencygraph - สร้างกราฟการพึ่งพาไลบรารีสำหรับไลบรารีในไดเร็กทอรีปัจจุบันdependency-all - สร้างกราฟการพึ่งพาสำหรับไลบรารี PVS ในโฟลเดอร์ปัจจุบันคลิกที่นี่เพื่อดูรายละเอียดเพิ่มเติมเกี่ยวกับสคริปต์เหล่านี้
(*) รวมอยู่ในการแจกจ่าย PVS 7.1 แล้ว
NASALib (v7.0.1) เข้ากันได้อย่างสมบูรณ์กับ VSCode-PVS ซึ่งเป็นอินเทอร์เฟซกราฟิกสมัยใหม่สำหรับ PVS ที่ใช้ Visual Studio Code NASALib เวอร์ชันล่าสุดสามารถติดตั้งได้จาก VSCode-PVS
สำหรับผู้ใช้ขั้นสูง PVS เวอร์ชันการพัฒนามีให้ใช้งานจาก GitHub หากต้องการโคลนเวอร์ชันการพัฒนา ให้พิมพ์คำสั่งต่อไปนี้ภายในไดเร็กทอรีที่ติดตั้ง PVS 7.0 ต่อจากนี้ไป ไดเร็กทอรีนั้นจะถูกเรียกว่า
$ git clone http://github.com/nasa/pvslib nasalib คำสั่งด้านบนจะวางสำเนาของไลบรารีไว้ในไดเร็กทอรี
ขณะนี้ groups ไลบรารีเลิกใช้แล้ว ห้องสมุด group ถูกรวมเข้ากับ algebra ลิงก์สัญลักษณ์ยังคงมีให้สำหรับความเข้ากันได้แบบย้อนหลัง แต่ไม่สนับสนุนการใช้งาน การกล่าวถึง groups ทุกครั้งควรถูกแทนที่ด้วย algebra
ไลบรารี trig_fnd เลิกใช้แล้ว มันยังคงมีไว้เพื่อความเข้ากันได้แบบย้อนหลัง แต่ควรจะแทนที่ด้วย trig trig ตรีโกณมิติใหม่ ซึ่งเคยเป็นสัจพจน์ กลายเป็นพื้นฐานแล้ว อย่างไรก็ตาม ตรงกันข้ามกับ trig_fnd คำจำกัดความเกี่ยวกับวิชาตรีโกณมิติจะขึ้นอยู่กับอนุกรมอนันต์ มากกว่าอินทิกรัล การเปลี่ยนแปลงนี้ช่วยลดการตรวจสอบประเภทของทฤษฎีที่เกี่ยวข้องกับฟังก์ชันตรีโกณมิติได้อย่างมาก การเปลี่ยนแปลงจาก trig_fnd เป็น trig ไม่ควรมีผลกระทบสำคัญต่อการพัฒนาอย่างเป็นทางการของคุณ เนื่องจากชื่อของคำจำกัดความและบทแทรกจะเหมือนกัน อย่างไรก็ตาม การนำเข้าตามทฤษฎีอาจแตกต่างกันเล็กน้อย
การพัฒนา PVS TCASII , WellClear และ DAIDALUS พร้อมใช้งานแล้วโดยเป็นส่วนหนึ่งของการเผยแพร่ GitHub WellClear PRECiSA การพัฒนา PVS พร้อมให้ใช้งานแล้วโดยเป็นส่วนหนึ่งของการแจกจ่าย GitHub PRECiSA PolyCARP การพัฒนา PVS พร้อมให้ใช้งานแล้วโดยเป็นส่วนหนึ่งของการแจกจ่าย GitHub PolyCARP
คำแนะนำต่อไปนี้จะถือว่า NASALib อยู่ในไดเร็กทอรี
PVS_LIBRARY_PATH หากไม่มีอยู่ ให้สร้างตัวแปรดังกล่าวและกำหนดให้เส้นทางของไดเร็กทอรีนี้เป็นเนื้อหาเท่านั้น โดยปกติแล้วจะมีประโยชน์มากหากระบบเชลล์ของคุณสร้างตัวแปรนี้เมื่อเริ่มต้นระบบ ด้วยเหตุนี้ และขึ้นอยู่กับเชลล์ของคุณ คุณอาจต้องการเพิ่มบรรทัดใดบรรทัดหนึ่งต่อไปนี้ในสคริปต์เริ่มต้นของคุณ สำหรับ C เชลล์ (csh หรือ tcsh) คุณสามารถเพิ่มบรรทัดนี้ใน ~/.cshrc :
setenv PVS_LIBRARY_PATH " /nasalib " สำหรับ Borne shell (bash หรือ sh) ให้เพิ่มบรรทัดนี้ใน ~/.bashrc หรือ ~/.profile :
export PVS_LIBRARY_PATH= " /nasalib " หากคุณมีการติดตั้ง NASALib ก่อนหน้านี้ ให้ลบไฟล์ ~/.pvs.lisp ออก หรือหากคุณมีการกำหนดค่าพิเศษในไฟล์นั้น ให้ลบบรรทัดต่อไปนี้
( load " /nasalib/pvs-patches.lisp " ) สุดท้าย ไปที่ไดเร็กทอรี
คำสั่ง install-scripts จะอัปเดตและติดตั้งสคริปต์ NASALib ตามความจำเป็น
$ ./install-scriptsNASALib เวอร์ชันเก่าหาได้จาก http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library
NASALib เติบโตขึ้นในช่วงหลายปีที่ผ่านมาด้วยการมีส่วนร่วมของบุคคลหลายคน ซึ่งได้แก่:
หากเราระบุแหล่งที่มาของการพัฒนา PVS อย่างไม่ถูกต้อง หรือคุณสนับสนุน NASALib และไม่ได้รวมชื่อของคุณไว้ที่นี่ โปรดแจ้งให้เราทราบ
หากคุณต้องการมีส่วนร่วมโปรดอ่านคู่มือนี้
NASALib คือชุดข้อกำหนดอย่างเป็นทางการซึ่งส่วนใหญ่อยู่ในสาธารณสมบัติมาหลายปีแล้ว ทีมวิธีการอย่างเป็นทางการของ NASA LaRC ยังคงรักษาการพัฒนาเหล่านี้ไว้ สำหรับการพัฒนาที่สร้างสรรค์โดยทีมวิธีการอย่างเป็นทางการ การพัฒนาเหล่านี้ถือเป็นการวิจัยพื้นฐานที่ไม่ประกอบด้วยซอฟต์แวร์ ผลงานที่ผู้อื่นทำอาจมีใบอนุญาตเฉพาะ ซึ่งแสดงอยู่ในไฟล์ top.pvs ในแต่ละไดเร็กทอรีที่เกี่ยวข้อง ในกรณีที่มีข้อสงสัย โปรดติดต่อผู้พัฒนาของแต่ละการสนับสนุนซึ่งมีรายชื่ออยู่ในไฟล์นั้นด้วย
แพตช์ PVS ซึ่งรวมอยู่ในไดเร็กทอรี pvs-patches เป็นส่วนหนึ่งของซอร์สโค้ด PVS และอยู่ภายใต้ใบอนุญาตโอเพ่นซอร์ส PVS
กลยุทธ์การพิสูจน์บางอย่างจำเป็นต้องใช้เครื่องมือวิจัยของบุคคลที่สาม เช่น MetiTarski และ Z3 เพื่อความสะดวก จึงรวมอยู่ในพื้นที่เก็บข้อมูลนี้โดยได้รับอนุญาตจากผู้เขียน สิทธิ์การใช้งานสำหรับเครื่องมือเหล่านี้ยังรวมอยู่ด้วยตามความเหมาะสม
สนุกกับมัน
ทีมวิธีการอย่างเป็นทางการที่ LaRC
เซซาร์ มูโนซ มาเรียโน มอสกาโต
