NASALib — это непрерывная совместная работа, продолжающаяся более 3 десятилетий, направленная на помощь в исследованиях, связанных с доказательством теорем, спонсируемых НАСА (https://shemesh.larc.nasa.gov/fm/pvs/). Он состоит из коллекции формальных разработок (то есть библиотек ), написанных в системе проверки прототипов (PVS), предоставленных SRI, NASA, NIA и сообществом PVS и поддерживаемых командой формальных методов в LaRC.
Текущая версия NASALib — 7.1.2 (01.09.2023), для нее требуется PVS 7.1.
В настоящее время NASALib состоит из 62 библиотек верхнего уровня , содержащих в общей сложности около 38 тысяч проверенных формул.
| Библиотека | Описание |
|---|---|
| СОГЛАСИЕ | Структура анализа алгоритмов обнаружения и разрешения конфликтов при воздушном движении |
| affine_arith | Формализация аффинной арифметики и стратегия вычисления полиномиальных функций с переменными в интервальных областях |
| алгебра | Группы, моноиды, кольца и т.д. |
| анализ | Реальный анализ, пределы, непрерывность, производные, интегралы |
| АСП | Денотационная семантика программирования набора ответов |
| авиация | Поддержка определений и свойств для формализаций, связанных с авиацией. |
| Бернштейн | Формализация многомерных полиномов Бернштейна |
| CCG | Формализация различных критериев прекращения |
| сложный | Комплексные числа |
| complex_alt | Альтернативная формализация комплексных чисел |
| complex_integration | Комплексная интеграция |
| со_структуры | Последовательности счетной длины, определенные как коалгебраические типы данных |
| диграфы | Ориентированные графы: схемы, максимальные поддеревья, пути, DAG. |
| дл | Дифференциальная динамическая логика |
| точный_реальный_ариф | Точная действительная арифметика, включая триггерные функции |
| примеры | Примеры применения функционала, предоставляемого NASALib |
| расширенный_nnreal | Расширенные неотрицательные числа |
| fast_approx | Приближения стандартных числовых функций |
| отказоустойчивость | Протоколы отказоустойчивости |
| плавать | Арифметика с плавающей запятой |
| графики | Теория графов |
| интервал_ариф | Интервальная арифметика и числовые аппроксимации. Включает автоматизированные числовые стратегии для вычисления численных аппроксимаций и интервал для проверки выполнимости и достоверности просто количественных формул с действительными значениями. Эта разработка включает формализацию временной логики интервалов Аллена. |
| целые числа | Целочисленное деление, НОД, мод, разложение на простые факторы, мин, макс |
| Лебег | Интеграл Лебега с привязкой к интегралу Римана |
| линейная_алгебра | Линейная алгебра |
| line_segments | 2-мерные сегменты линий |
| Инэксп | Логарифмы, показательные и гиперболические функции. & Основные определения логарифма, показательной и гиперболической функций |
| литы | Линейная временная логика |
| матрицы | Исполняемая спецификация матриц MxN. Эта библиотека включает в себя вычисление обратных и основных матричных операций, таких как сложение и умножение. |
| Measure_integration | Сигма-алгебры, меры, леммы Фубини-Тонелли |
| МетиТарский | Интеграция MetiTarski, автоматизированного средства доказательства теорем для вещественных функций. |
| метрическое_пространство | Области с метрикой расстояния, непрерывностью и равномерной непрерывностью |
| мв_анализ | Многомерный реальный анализ: нормы, пределы, непрерывность, производные, оптимизация и т. д. |
| mult_poly | Многомерные полиномы и полуалгебраические множества. |
| номинальный | Номинальное уравнение |
| цифры | Элементарная теория чисел |
| ОДУ | Обыкновенные дифференциальные уравнения |
| заказы | Абстрактные порядки, решетки, фиксированные точки |
| многоугольники | 2-мерные многоугольники |
| многоугольник_слияние | Объединение двумерных полигонов без создания дыр |
| власть | Обобщенная степенная функция (без ln/exp) |
| вероятность | Теория вероятностей |
| ПВС0 | Формализация фундаментальных концепций вычислимости |
| pvsio_utils | Дополнения к PVSio, стандартной библиотеке PVS для анимации спецификаций PVS. |
| Реалы | Суммирование, sup, inf, sqrt по действительным значениям, абсолютное значение и т. д. |
| Риман | Интеграл Римана |
| Скотт | Топология Скотта |
| ряд | Степенной ряд, критерий сравнения, критерий отношения, теорема Тейлора |
| set_aux | Степенные множества, порядки, мощность над бесконечными множествами. Включает функциональные и реляционные факты, основанные на аксиоме выбора, и уточняющие отношения, основанные на отношениях эквивалентности. |
| формы | 2D-фигуры: треугольник, параллелограмм, прямоугольник, сегмент окружности. |
| сигма_set | Суммирование по счетным бесконечным множествам |
| сортировка | Алгоритмы сортировки |
| структуры | Ограниченные массивы, конечные последовательности, пакеты и некоторые другие структуры. |
| Штурм | Формализация теоремы Штурма для одномерных многочленов. Включает стратегии sturm и mono-poly для автоматического доказательства одномерных полиномиальных отношений на реальном интервале. |
| Тарский | Формализация теоремы Тарского для одномерных многочленов. Включает стратегию Тарского для автоматического доказательства систем одномерных полиномиальных отношений на реальной прямой. |
| топология | Непрерывность, гомеоморфизмы, связные и компактные пространства, борелевские множества/функции. |
| триггер | Тригонометрия: определения, тождества, приближения |
| ТРС | Системы перезаписи терминов и алгоритм унификации Робинсона |
| TU_games | Кооперативные ТУ-игры |
| vect_anaанализ | Пределы, непрерывность и производные векторных функций |
| векторы | 2D, 3D, 4D и n-мерные векторы |
| пока | Семантика языка программирования |
NASALib также предоставляет набор скриптов, автоматизирующих несколько задач.
proveit (*) - Запускает PVS в пакетном режимеprovethem (*) — Запускает proveit в нескольких библиотеках.pvsio (*) — утилита командной строки для запуска наземного оценщика PVSio.prove-all — запускает proveit в каждой библиотеке в NASALib, обертывая provethem , чтобы обеспечить определенный тип запуска.cleanbin-all — очистить .pvscontext и двоичные файлы из библиотек PVS.find-all — ищет строки, соответствующие заданным регулярным выражениям в библиотеках PVS.dependencygraph — генерирует график зависимостей библиотек в текущем каталоге.dependency-all — генерирует графики зависимостей для библиотек PVS в текущей папке.Нажмите здесь, чтобы получить более подробную информацию об этих сценариях.
(*) Уже включен в дистрибутив PVS 7.1.
NASALib (v7.0.1) полностью совместима с VSCode-PVS, современным графическим интерфейсом для PVS, основанным на коде Visual Studio. Последнюю версию NASALib можно установить из VSCode-PVS.
Для опытных пользователей PVS версия для разработки доступна на GitHub. Чтобы клонировать версию разработки, введите следующую команду в каталоге, где установлен PVS 7.0. В дальнейшем этот каталог будет называться
$ git clone http://github.com/nasa/pvslib nasalib Приведенная выше команда поместит копию библиотеки в каталог
groups библиотек больше не поддерживаются . group библиотека была интегрирована в algebra . Символическая ссылка по-прежнему предоставляется для обратной совместимости, но ее использование не рекомендуется. Каждое упоминание groups следует заменять algebra .
Библиотека trig_fnd устарела . Он по-прежнему предусмотрен для обратной совместимости, но его следует заменить на trig . Новая библиотека trig , которая раньше была аксиомой, теперь является основополагающей. Однако, в отличие от trig_fnd , тригонометрические определения основаны на бесконечных рядах, а не на интегралах. Это изменение значительно упрощает проверку типов теорий, включающих тригонометрические функции. Изменение с trig_fnd на trig не должно иметь большого влияния на ваши формальные разработки, поскольку имена определений и лемм одинаковы. Однако импорт теории может немного отличаться.
Разработки PVS TCASII , WellClear и DAIDALUS теперь доступны как часть дистрибутива GitHub WellClear. Разработка PVS PRECiSA теперь доступна как часть дистрибутива PRECiSA на GitHub. Разработка PolyCARP для PVS теперь доступна как часть дистрибутива PolyCARP на GitHub.
В следующих инструкциях предполагается, что NASALib находится в каталоге
PVS_LIBRARY_PATH Если он не существует, создается такая переменная, в которой в качестве содержимого используется только путь к этому каталогу. Обычно очень полезно, чтобы ваша система оболочки создавала эту переменную при запуске. С этой целью и в зависимости от вашей оболочки вы можете добавить одну из следующих строк в свой сценарий запуска. Для оболочки C (csh или tcsh) вы можете добавить эту строку в ~/.cshrc :
setenv PVS_LIBRARY_PATH " /nasalib " Для оболочки Borne (bash или sh) добавьте эту строку в ~/.bashrc или ~/.profile :
export PVS_LIBRARY_PATH= " /nasalib " Если у вас была предыдущая установка NASALib, либо удалите файл ~/.pvs.lisp , либо, если в этом файле есть специальная конфигурация, удалите следующую строку
( load " /nasalib/pvs-patches.lisp " ) Наконец, перейдите в каталог
Команда install-scripts обновит и установит сценарии NASALib по мере необходимости.
$ ./install-scriptsБолее старые версии NASALib доступны по адресу http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library.
NASALib с годами выросла благодаря вкладу нескольких человек, среди них:
Если мы ошибочно приписали разработку PVS или вы внесли свой вклад в NASALib и ваше имя здесь не указано, сообщите нам об этом.
Если вы хотите внести свой вклад, прочтите это руководство.
NASALib представляет собой набор официальных спецификаций, большинство из которых уже несколько лет находятся в открытом доступе. Команда формальных методов NASA LaRC до сих пор поддерживает эти разработки. Для разработок, первоначально сделанных командой формальных методов, эти разработки считаются фундаментальными исследованиями, которые не представляют собой программное обеспечение. Вклады других лиц могут иметь определенные лицензии, которые перечислены в файле top.pvs в каждом соответствующем каталоге. В случае сомнений свяжитесь с разработчиками каждого вклада, которые также указаны в этом файле.
Патчи PVS, включенные в каталог pvs-patches , являются частью исходного кода PVS и на них распространяется лицензия с открытым исходным кодом PVS.
Для некоторых стратегий доказательства требуются сторонние исследовательские инструменты, например MetiTarski и Z3. Для удобства они включены в этот репозиторий с разрешения их авторов. Лицензии на эти инструменты также включены по мере необходимости.
Наслаждайся этим.
Команда формальных методов в LaRC
Сезар Муньос Мариано Москато
