프로토타입 검증 시스템

프로토타입 검증 시스템(PVS)은 캘리포니아 주 멘로파크에 있는 SRI 인터내셔널 컴퓨터과학연구소에서 개발한 지원 도구와 자동 정리 프로베렐이 통합된 사양 언어다.

PVS는 의존형 타입을 가진 타입 이론의 확장으로 구성된 커널을 기반으로 하며, 근본적으로 고전적인 타입의 고차원의 논리다.기본 형식은 사용자가 도입할 수 있는 해석되지 않은 형식과 술래, 정수, 리얼, 서수 등 빌트인 형식을 포함한다.유형 구성자에는 함수, 집합, 튜플, 레코드, 열거 및 추상 데이터 유형이 포함된다.술어 하위 유형과 종속 유형은 구속조건을 도입하는 데 사용될 수 있다. 이러한 제약된 유형은 유형 확인 중에 입증 의무(유형 수정 조건 또는 TCC라고 함)를 발생시킬 수 있다.PVS 규격은 매개변수화된 이론으로 구성된다.

이 시스템은 Common Lisp에서 구현되며 GNU General Public License(GPL)에 따라 출시된다.

참고 항목

• 형식 방법

참조

• 오와르, 샨카, 1992년 러시비PVS: 프로토타입 검증 시스템.CADE 11 회의 절차에 발표됨.

외부 링크

• SRI 인터내셔널 컴퓨터 과학 연구소의 PVS 웹사이트
• Michael Kholhase와 Carolyn Talcott의 기계화 추론 데이터베이스에서 John Rushby가 PVS 요약