pvslib

美國太空總署圖書館

NASALib 是一項跨越 30 多年的持續合作成果，旨在協助 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個頂級庫組成，總共包含約38K個經過驗證的公式。

圖書館	描述
符合	空中交通衝突偵測與解決演算法分析框架
仿射_arith	仿射算術的形式化和評估具有區間域變數的多項式函數的策略
代數	群、廬半群、環等
分析	實分析、極限、連續性、導數、積分
ASP	答案集編程的指稱語義
航空	支持航空相關形式化的定義和屬性
伯恩斯坦	多元伯恩斯坦多項式的形式化
CCG	多樣化終止標準的形式化
複雜的	複數
複雜的替代品	複數的替代形式化
複雜的整合	複雜的集成
協同結構	定義為餘代數資料型別的可數長度序列
有向圖	有向圖：電路、最大子樹、路徑、DAG
dL	微分動態邏輯
精確實數	精確的實數算術，包括三角函數
例子	NASALib提供的功能的應用範例
擴充_nnreal	擴展非負實數
快速近似	標準數值函數的近似值
容錯	容錯協議
漂浮	浮點運算
圖表	圖論
間隔算術	區間算術和數值近似。包括用於計算數值近似值的自動化數值策略和用於檢查簡單量化實值公式的可滿足性和有效性的區間。這項發展包括艾倫區間時序邏輯的形式化
整數	整數除法、gcd、mod、素因數分解、最小值、最大值
勒貝格	勒貝格積分與黎曼積分的聯繫
線性代數	線性代數
線段	二維線段
指數	對數、指數和雙曲函數。 & 對數、指數與雙曲函數的基本定義
零擔運輸	線性時態邏輯
矩陣	MxN 矩陣的可執行規範。該庫包括逆計算和基本矩陣運算，例如加法和乘法
測量整合	西格瑪代數、測度、Fubini-Tonelli 引理
梅蒂·塔斯基	整合 MetiTarski（實值函數的自動定理證明器）
度量空間	具有距離測量、連續性和一致連續性的域
MV_分析	多元實數分析：範數、極限、連續性、導數、最佳化等。
多聚	多元多項式和半代數集。
名義上的	名目等式推理
數位	初等數論
常微分方程	常微分方程
訂單	抽象階、格、不動點
多邊形	二維多邊形
多邊形合併	合併二維多邊形而不產生孔
力量	廣義冪函數（不含 ln/exp）
可能性	機率論
PVS0	基本可計算性概念的形式化
pvsio_utils	PVSio 的補充，PVS 標準庫，用於 PVS 規範的動畫
雷亞爾	求和、sup、inf、實數開方、絕對值等
黎曼	黎曼積分
史考特	斯科特拓撲
系列	冪級數、比較檢定、比率檢定、泰勒定理
組輔助	冪集、階數、無限集上的基數。包括基於選擇公理的功能和關係事實以及基於等價關係的細化關係
形狀	2D 形狀：三角形、平行四邊形、長方形、圓弧
西格瑪集	可數無限集的求和
排序	排序演算法
結構	有界數組、有限序列、套件和其他幾種結構
斯圖姆	單變數多項式的 Sturm 定理的形式化。包括用於在實數區間自動證明單變量多項式關係的策略sturm和mono-poly
塔斯基	單變量多項式塔斯基定理的形式化。包括用於自動證明實線上單變量多項式關係系統的策略 tarski
拓樸結構	連續性、同胚、連通空間與緊空間、Borel 集/函數
三角函數	三角學：定義、恆等式、近似值
TRS	術語重寫系統和羅賓遜統一演算法
TU_遊戲	合作TU博弈
向量分析	向量函數的極限、連續性與導數
向量	2-D、3-D、4-D 和 n 維向量
儘管	程式語言的語意 While

結構

腳本

NASALib 也提供了一組可自動執行多項任務的腳本。

• proveit (*) - 以批次模式運行 PVS
• provethem (*) - 在多個庫上運行proveit
• pvsio (*) - 用於執行 PVSio 地面評估器的命令列公用程式。
• prove-all - 通過包裝provethem來在 NASALib 中的每個庫上proveit證明，以提供特定類型的運行。
• cleanbin-all - 從 PVS 庫清理.pvscontext和二進位檔案。
• find-all - 在 PVS 庫中搜尋與給定正規表示式相符的字串。
• dependencygraph - 為目前目錄中的庫產生庫依賴關係圖。
• dependency-all - 產生目前資料夾中的 PVS 庫的依賴關係圖。

按此處了解有關這些腳本的更多詳細資訊。

(*) 已包含在 PVS 7.1 發行版中。

取得 NASALib

透過VSCode-PVS（推薦PVS新用戶）

NASALib (v7.0.1) 與 VSCode-PVS 完全相容，VSCode-PVS 是基於 Visual Studio Code 的現代 PVS 圖形介面。可以從 VSCode-PVS 安裝最新版本的 NASALib。

開發版

對於 PVS 高級用戶，可以從 GitHub 取得開發版本。若要複製開發版本，請在安裝 PVS 7.0 的目錄中鍵入下列命令。此後，該目錄將被稱為<pvsdir> 。下面的命令中，美元符號代表作業系統的提示符號。

$ git clone http://github.com/nasa/pvslib nasalib 

上面的指令會將庫的副本放入目錄<pvsdir>/nasalib中。

最近的主要變化

• 庫groups現已棄用。 group庫已整合到algebra中。仍提供符號連結以實現向後相容性，但不鼓勵使用它。每次提到groups都應該用algebra代替。

• 庫trig_fnd現已棄用。它仍然是為了向後相容而提供的，但它應該被trig取代。新的庫trig曾經是公理化的，現在是基礎性的。然而，與trig_fnd相比，三角函數定義是基於無窮級數，而不是積分。這一變化大大減少了涉及三角函數的理論的類型檢查。從trig_fnd到trig的變更不會對您的正式開發產生重大影響，因為定義和引理的名稱是相同的。然而，理論導入可能略有不同。

• PVS 開發的TCASII 、 WellClear和DAIDALUS現已作為 GitHub WellClear 發行版的一部分提供。 PVS 開發PRECiSA現已作為 GitHub PRECiSA 發行版的一部分提供。 PVS 開發PolyCARP現已作為 GitHub PolyCARP 發行版的一部分提供。

手動安裝

以下說明假設 NASALib 位於目錄<pvsdir>/nasalib中。

1）將此目錄加入到環境變數PVS_LIBRARY_PATH中

如果不存在，則建立該變數並以此目錄的路徑作為唯一內容。讓 shell 系統在啟動時建立此變數通常非常有用。為此，根據您的 shell，您可能需要在啟動腳本中添加以下行之一。對於 C shell（csh 或 tcsh），您可以在~/.cshrc中新增此行：

setenv PVS_LIBRARY_PATH " <pvsdir>/nasalib "

對於 Borne shell（bash 或 sh），請在~/.bashrc或~/.profile中新增以下行：

 export PVS_LIBRARY_PATH= " <pvsdir>/nasalib " 

2) 保護先前的 NASALib 配置的附加步驟（可選）

如果您以前安裝過 NASALib，請刪除檔案~/.pvs.lisp ，或者如果您在該檔案中有特殊配置，請刪除以下行

( load " <pvsdir>/nasalib/pvs-patches.lisp " ) 

3）安裝腳本

最後進入<pvsdir>/nasalib目錄，執行以下shell腳本（美元符號代表作業系統的提示符號）。

install-scripts命令將根據需要更新和安裝 NASALib 腳本。

$ ./install-scripts

舊版

舊版的 NASALib 可從 http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library 取得。

貢獻者

NASALib 多年來的發展得益於許多人的貢獻，包括：

• 亞倫杜特爾，美國太空總署
• Alfons Geser，HTWK 萊比錫，德國
• Amer Tahat，美國密西根理工大學
• Amy Isvik，美國瓦特堡學院
• Ana Cristina Rocha Oliveira，巴西巴西利亞大學
• André Luiz Galdino，巴西加泰隆尼亞聯邦大學
• 安德烈亞‧阿韋拉爾‧博爾赫斯，巴西巴西利亞大學
• Anthony Narkawicz，前美國國家航空暨太空總署 (NASA)
• 阿麗亞娜‧阿爾維斯‧阿爾梅達，巴西巴西利亞大學
• 布魯諾杜特蒂，SRI，美國
• Ben Di Vito，美國太空總署（已退休）
• Ben Hocking，可靠計算，美國
• 塞薩爾·穆尼奧斯，美國太空總署
• Clément Blaudeau，瑞士洛桑聯邦理工學院和法國巴黎綜合理工學院
• 康塞普西翁維達爾，拉科魯尼亞大學，西班牙
• David Griffioen，CWI，荷蘭
• 大衛萊斯特，英國曼徹斯特大學
• 德拉甘·斯托西奇，愛爾蘭
• Érik Martin-Dorel，蒙彼利埃大學 2 和佩皮尼昂大學（前），法國
• 艾絲特‧康拉德，美國太空總署
• Felicidad Aguado，拉科魯尼亞大學，西班牙
• Flavio LC de Moura，巴西巴西利亞大學
• 加布里埃爾·費雷拉·席爾瓦，巴西巴西利亞大學
• Gilles Dowek，INRIA，法國
• 喬治哈根，美國太空總署
• Gilberto Perez，西班牙拉科魯尼亞大學
• 葛瑞格里安德森，德州大學奧斯汀分校，美國
• Hanne Gottliebsen，曾在美國 NIA 工作
• Heber Herencia-Zapana，曾在美國 NIA 工作
• J. Tanner Slagel，美國太空總署
• Jerry James，美國猶他州立大學
• 傑夫馬達隆，美國太空總署
• 喬恩‧舍格倫，美國國防部
• John Siratt，曾就讀於美國阿肯色大學小石城分校
• 凱瑟琳·科德威爾，卡內基美隆大學，美國
• 克莉絲汀‧羅齊爾 (Kristin Rozier)，曾任職於美國太空總署
• Laura Titolo，AMA Inc. 和 NASA，美國
• Lee Pike，曾任職於美國太空總署
• Marco A. Feliú，AMA Inc.，美國
• 馬裡亞諾·莫斯卡托，AMA Inc.，美國
• Mauricio Ayala-Rincón，巴西巴西利亞大學
• Natarajan Shankar，SRI，美國
• Pablo Ascariz，原西班牙拉科魯尼亞大學
• Paolo Masci，AMA Inc. 和 NASA，美國
• 保羅‧邁納，美國太空總署
• 佩德羅·卡巴拉爾，拉科魯尼亞大學，西班牙
• Radu Siminiceanu，前美國 NIA
• 瑞奇巴特勒 (Ricky Butler)，美國太空總署（已退休）
• Silvie Boldo，INRIA，法國
• Sam Owre，SRI，美國
• Thaynara Arielly de Lima，巴西戈亞斯聯邦大學
• 蒂亞戈·門東薩·費雷拉·拉莫斯，巴西巴西利亞大學
• 托馬斯·諾里斯
• Víctor Carreño，美國太空總署（已退休）
• 華盛頓·路易斯·裡貝羅·德卡瓦略第二，巴西巴西利亞大學

如果我們錯誤地歸因了 PVS 開發，或者您為 NASALib 做出了貢獻，但您的名字未包含在此處，請告知我們。

如果您想做出貢獻，請閱讀本指南。

免責聲明

NASALib 是正式規範的集合，其中大部分已在公共領域公開多年。 NASA LaRC 的形式方法團隊仍然保持著這些發展。對於形式化方法團隊最初進行的開發，這些開發被認為是不構成軟體的基礎研究。其他人所做的貢獻可能具有特定的許可證，這些許可證列在每個目錄的top.pvs檔案中。如有疑問，請聯絡每個貢獻的開發人員，這些開發人員也列在該文件中。

PVS 補丁包含在pvs-patches目錄中，是 PVS 原始碼的一部分，並由 PVS 開源許可證涵蓋。

一些證明策略需要第三方研究工具，例如 MetiTarski 和 Z3。為了方便起見，它們經過作者的許可包含在這個儲存庫中。這些工具的許可證也包含在適當的情況下。

好好享受。

LaRC 的形式化方法團隊

維護者

塞薩爾·穆尼奧斯·馬裡亞諾·莫斯卡托