Система проверки прототипа - Prototype Verification System

Скриншот PVS

Система проверки прототипов ( PVS ) - это язык спецификаций, интегрированный с инструментами поддержки и автоматическим средством доказательства теорем , разработанный в Лаборатории компьютерных наук SRI International в Менло-Парке, Калифорния .

PVS основан на ядре, состоящем из расширения теории типов Чёрча с зависимыми типами , и по сути является классической типизированной логикой высшего порядка. Базовые типы включают в себя неинтерпретируемые типы, которые могут быть введены пользователем, и встроенные типы, такие как логические, целые, действительные и порядковые. Конструкторы типов включают в себя функции, множества, кортежи, записи, перечисления и абстрактные типы данных. Подтипы предикатов и зависимые типы могут использоваться для введения ограничений; эти ограниченные типы могут нести обязательства по проверке (называемые условиями корректности типа или TCC) во время проверки типов. Спецификации PVS организованы в параметризованные теории.

Система реализована на Common Lisp и выпущена под лицензией GNU General Public License (GPL).

Смотрите также

Ссылки

  • Оуре , Шанкар и Рашби , 1992. PVS: система проверки прототипа . Опубликовано в сборнике материалов конференции CADE 11 .

внешняя ссылка