Система проверки прототипа

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

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

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

См. также [ править ]

Ссылки [ править ]

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

Внешние ссылки [ править ]

Веб-сайт PVS в SRI International лаборатории компьютерных наук
Краткое изложение PVS Джона Рашби в Mechanized Reasoning базе данных Майкла Кольхейза и Кэролин Талкотт

Эта языкам программирования, статья, посвященная является незавершенной . Вы можете помочь Википедии, расширив ее .

Эта логике статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее .