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