Войти
Снимок экрана PVS Система проверки прототипа (PVS ) - это язык спецификаций, интегрированный с инструментами поддержки и автоматическим средством доказательства теорем, разработанный в Лаборатории компьютерных наук SRI International в Менло-Парк, Калифорния.
PVS основан на ядре, состоящем из расширения теории типов Черча с зависимыми типами, и по сути является классическим типизированным логика высшего порядка. Базовые типы включают неинтерпретируемые ed типы, которые могут быть введены пользователем, и встроенные типы, такие как логические, целые, действительные и порядковые. Конструкторы типов включают в себя функции, множества, кортежи, записи, перечисления и абстрактные типы данных. Подтипы предикатов и зависимые типы могут использоваться для введения ограничений; эти ограниченные типы могут нести обязательства по проверке (называемые условиями корректности типа или TCC) во время проверки типов. Спецификации PVS организованы в параметризованные теории.
Система реализована на Common Lisp и выпущена под Стандартной общественной лицензией GNU (GPL).
.
