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