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

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