NASALib는 NASA(https://shemesh.larc.nasa.gov/fm/pvs/)가 후원하는 정리 증명 관련 연구를 지원하기 위해 30년 이상 지속된 지속적인 공동 노력입니다. 이는 프로토타입 검증 시스템(PVS)으로 작성되고 SRI, NASA, NIA 및 PVS 커뮤니티에서 기여하고 LaRC의 형식 방법 팀에서 유지 관리하는 공식 개발 모음(예: 라이브러리 )으로 구성됩니다.
NASALib의 현재 버전은 7.1.2(2023/09/01)이며 PVS 7.1이 필요합니다.
현재 NASALib은 총 약 38,000개의 입증된 공식을 포함하는 62개의 최상위 라이브러리로 구성되어 있습니다.
| 도서관 | 설명 |
|---|---|
| 일치 | 항공 교통 충돌 감지 및 해결 알고리즘 분석을 위한 프레임워크 |
| affine_arith | 구간 영역의 변수를 사용하여 다항식 함수를 평가하기 위한 아핀 연산의 형식화 및 전략 |
| 대수학 | 그룹, 모노이드, 링 등 |
| 분석 | 실수 분석, 극한, 연속성, 도함수, 적분 |
| ASP | 응답 세트 프로그래밍의 표시 의미 |
| 비행 | 항공 관련 형식화에 대한 정의 및 속성 지원 |
| 번스타인 | 다변량 Bernstein 다항식의 공식화 |
| CCG | 다양한 종료 기준의 공식화 |
| 복잡한 | 복소수 |
| complex_alt | 복소수의 대체 형식화 |
| 단지_통합 | 복잡한 통합 |
| 공동 구조 | 공동대수 데이터 유형으로 정의된 셀 수 있는 길이의 시퀀스 |
| 이중문자 | 방향 그래프: 회로, 최대 하위 트리, 경로, DAG |
| dL | 차동 동적 논리 |
| 정확한_실제_산식 | 삼각 함수를 포함한 정확한 실수 연산 |
| 예 | NASALib에서 제공하는 기능 적용 사례 |
| Extended_nnreal | 음수가 아닌 확장된 실수 |
| fast_about | 표준 수치 함수의 근사치 |
| 내결함성 | 내결함성 프로토콜 |
| 뜨다 | 부동 소수점 연산 |
| 그래프 | 그래프 이론 |
| 간격_산 | 간격 산술 및 수치 근사. 단순히 정량화된 실제 값 공식의 만족도와 타당성을 확인하기 위한 수치 근사치 및 간격을 계산하기 위한 자동화된 수치 전략이 포함되어 있습니다. 이 개발에는 Allen 간격 시간 논리의 공식화가 포함됩니다. |
| 정수 | 정수 나누기, gcd, mod, 소인수분해, 최소, 최대 |
| 르베그 | 리만 적분과 연결된 르베그 적분 |
| 선형_대수학 | 선형대수학 |
| line_segments | 2차원 선분 |
| lnexp | 로그, 지수 및 쌍곡선 함수. 로그, 지수 및 쌍곡선 함수의 기본 정의 |
| LTL | 선형 시간 논리 |
| 행렬 | MxN 행렬의 실행 가능한 사양입니다. 이 라이브러리에는 덧셈, 곱셈과 같은 역행렬 및 기본 행렬 연산 계산이 포함되어 있습니다. |
| 측정_통합 | 시그마 대수학, 측정값, Fubini-Tonelli Lemmas |
| 메티타르스키 | 실수값 함수에 대한 자동화된 정리 증명인 MetiTarski 통합 |
| 미터법 공간 | 거리 측정법, 연속성 및 균일한 연속성을 갖춘 도메인 |
| mv_분석 | 다변량 실제 분석: 규범, 한계, 연속성, 도함수, 최적화 등 |
| 다중 폴리 | 다변량 다항식 및 반대수 집합. |
| 명사 같은 | 명목 방정식 추론 |
| 숫자 | 초등 정수론 |
| ODE | 상미분 방정식 |
| 명령 | 추상 주문, 격자, 고정점 |
| 다각형 | 2차원 다각형 |
| 다각형_병합 | 구멍을 생성하지 않고 2차원 다각형 병합 |
| 힘 | 일반화된 검정력 함수(ln/exp 제외) |
| 개연성 | 확률 이론 |
| PVS0 | 기본적인 계산 가능성 개념의 공식화 |
| pvsio_utils | PVS 사양 애니메이션을 위한 PVS 표준 라이브러리인 PVSio에 추가 |
| 진짜 | 실수에 대한 합계, sup, inf, sqrt, 절대값 등 |
| 리만 | 리만 적분 |
| 스캇 | 스콧 토폴로지 |
| 시리즈 | 멱급수, 비교 검정, 비율 검정, 테일러의 정리 |
| 세트_aux | 무한 집합에 대한 거듭제곱 집합, 차수, 카디널리티. 선택 공리(Axiom of Choice)에 기반한 기능적, 관계적 사실과 등가 관계에 기반한 정제 관계를 포함합니다. |
| 모양 | 2D 모양: 삼각형, 평행사변형, 직사각형, 원형 세그먼트 |
| 시그마_세트 | 셀 수 있는 무한 집합에 대한 합 |
| 정렬 | 정렬 알고리즘 |
| 구조물 | 제한된 배열, 유한 시퀀스, 가방 및 기타 여러 구조 |
| 스투름 | 일변량 다항식에 대한 Sturm의 정리의 공식화. 실제 간격에 걸쳐 일변량 다항식 관계를 자동으로 증명하기 위한 sturm 및 mono-poly 전략을 포함합니다. |
| 타르스키 | 일변량 다항식에 대한 Tarski 정리의 형식화. 실제 선에서 일변량 다항식 관계 시스템을 자동으로 증명하기 위한 전략 tarski가 포함되어 있습니다. |
| 토폴로지 | 연속성, 동형, 연결되고 컴팩트한 공간, Borel 세트/기능 |
| 삼각 | 삼각법: 정의, 항등식, 근사치 |
| TRS | 용어 재작성 시스템 및 Robinson 통합 알고리즘 |
| TU_games | 협동 TU 게임 |
| vect_분석 | 벡터 함수의 극한, 연속성 및 도함수 |
| 벡터 | 2차원, 3차원, 4차원 및 n차원 벡터 |
| ~하는 동안 | 프로그래밍 언어의 의미 체계 |
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(v7.0.1)은 Visual Studio Code를 기반으로 하는 PVS에 대한 최신 그래픽 인터페이스인 VSCode-PVS와 완벽하게 호환됩니다. 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 배포판의 일부로 제공됩니다. PVS 개발 PRECiSA 이제 GitHub PRECiSA 배포판의 일부로 제공됩니다. PVS 개발 PolyCARP 이제 GitHub PolyCARP 배포판의 일부로 제공됩니다.
다음 지침에서는 NASALib이
PVS_LIBRARY_PATH 에 추가합니다. 존재하지 않는 경우 해당 변수를 생성하고 이 디렉터리의 경로를 콘텐츠로만 사용합니다. 일반적으로 쉘 시스템이 시작 시 이 변수를 생성하도록 하는 것은 매우 유용합니다. 이를 위해 쉘에 따라 시작 스크립트에 다음 행 중 하나를 추가할 수 있습니다. C 셸(csh 또는 tcsh)의 경우 ~/.cshrc 에 다음 줄을 추가할 수 있습니다.
setenv PVS_LIBRARY_PATH " /nasalib " Borne 셸(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의 공식 방법 팀은 여전히 이러한 개발을 유지하고 있습니다. 원래 Formal Methods 팀이 수행한 개발의 경우 이러한 개발은 소프트웨어를 구성하지 않는 기초 연구로 간주됩니다. 다른 사람이 기여한 내용에는 특정 라이센스가 있을 수 있으며, 이는 각 디렉토리의 top.pvs 파일에 나열되어 있습니다. 의심스러운 경우 해당 파일에도 나열된 각 기여의 개발자에게 문의하세요.
pvs-patches 디렉터리에 포함된 PVS 패치는 PVS 소스 코드의 일부이며 PVS 오픈 소스 라이선스가 적용됩니다.
일부 증명 전략에는 MetiTarski 및 Z3와 같은 타사 연구 도구가 필요합니다. 편의를 위해 저자의 허가를 받아 이 저장소에 포함되었습니다. 이러한 도구에 대한 라이센스도 적절하게 포함됩니다.
즐겨보세요.
LaRC의 형식적 방법 팀
세자르 무뇨스 마리아노 모스카토
