Система проверки прототипа - Prototype Verification System
Система проверки прототипов ( PVS ) - это язык спецификаций, интегрированный с инструментами поддержки и автоматическим средством доказательства теорем , разработанный в Лаборатории компьютерных наук SRI International в Менло-Парке, Калифорния .
PVS основан на ядре, состоящем из расширения теории типов Чёрча с зависимыми типами , и по сути является классической типизированной логикой высшего порядка. Базовые типы включают в себя неинтерпретируемые типы, которые могут быть введены пользователем, и встроенные типы, такие как логические, целые, действительные и порядковые. Конструкторы типов включают в себя функции, множества, кортежи, записи, перечисления и абстрактные типы данных. Подтипы предикатов и зависимые типы могут использоваться для введения ограничений; эти ограниченные типы могут нести обязательства по проверке (называемые условиями корректности типа или TCC) во время проверки типов. Спецификации PVS организованы в параметризованные теории.
Система реализована на Common Lisp и выпущена под лицензией GNU General Public License (GPL).
Смотрите также
Ссылки
- Оуре , Шанкар и Рашби , 1992. PVS: система проверки прототипа . Опубликовано в сборнике материалов конференции CADE 11 .
внешняя ссылка
- Сайт PVS в Лаборатории компьютерных наук SRI International
- Резюме ПВСА от Джона Рашби на механизированном Рассуждении базе данных Майкла Kohlhase и Каролин Талкотт
Это язык программирования о связанной статье заглушка . Вы можете помочь Википедии, расширив ее . |
Эта статья о логике - незавершенная . Вы можете помочь Википедии, расширив ее . |