stringtranslate.com

Матита

Matita [1] — экспериментальный помощник по доказательству, разрабатываемый на кафедре компьютерных наук Болонского университета . Это инструмент, помогающий разрабатывать формальные доказательства посредством взаимодействия человека и машины, предоставляющий среду программирования, в которой естественным образом сосуществуют формальные спецификации , исполняемые алгоритмы и автоматически проверяемые сертификаты корректности.

Матита основана на системе зависимых типов , известной как исчисление (ко)индуктивных конструкций (производная от исчисления конструкций ), и в некоторой степени совместима с Coq .

Слово «matita» означает «карандаш» на итальянском языке (простой и распространенный инструмент редактирования). Это достаточно небольшое и простое приложение, [2] архитектурная и программная сложность которого должна быть освоена студентами, предоставляя инструмент, особенно подходящий для тестирования инновационных идей и решений. Matita использует режим редактирования на основе тактики; ( XML -кодированные) объекты доказательства создаются для хранения и обмена.

Основные характеристики

Экзистенциальные переменные являются собственными в Matita, что позволяет упростить управление зависимыми целями. [3]

Матита реализует двунаправленный алгоритм вывода типов [4], используя как выводимые, так и ожидаемые типы.

Мощность системы вывода типов (уточнения) дополнительно увеличивается за счет механизма подсказок [5] , который помогает синтезировать унификаторы в конкретных ситуациях, указанных пользователем.

Matita поддерживает сложную стратегию устранения неоднозначности [6], основанную на диалоге между синтаксическим анализатором и средством проверки типов .

На интерактивном уровне система реализует поэтапное выполнение структурированных тактик [7], что позволяет значительно улучшить управление разработкой доказательств и, естественно, приводит к созданию более структурированных и читаемых сценариев.

Приложения

Матита работала в CerCo (Certified Complexity): европейском проекте FP7, направленном на разработку формально проверенного , сохраняющего сложность компилятора с большого подмножества языка C на язык ассемблера микропроцессора MCS -51 .

Документация

Учебное пособие Matita [8] дает практическое введение в основные функции интерактивного устройства доказательства теорем Matita, предлагая пошаговый обзор набора нетривиальных примеров в области спецификации и верификации программного обеспечения .

Смотрите также

Ссылки

  1. ^ Андреа Асперти, Уилмер Риччиотти, Клаудио Сакердоти Коэн, Энрико Тасси. «Интерактивное средство доказательства теорем Matita»: CADE-23, LNCS 6803, 2011, стр. 64–69.
  2. ^ Асперти, А.; Риччиотти, В.; Сасердоти Коэн, К.; Тасси, Э. (2009). «Компактное ядро ​​для исчисления индуктивных конструкций». Садхана . 34 : 71–144. дои : 10.1007/s12046-009-0003-3 .
  3. ^ Андреа Асперти, Уилмер Риччиотти, К. Сакердоти Коэн, Энрико Тасси. «Новый тип тактики»: Технический отчет УБЛКС-2009-14. Июнь 2009 года.
  4. ^ Андреа Асперти, Вильмер Риччиотти, К. Сачердоти Коэн, Энрико Тасси. «Двунаправленный алгоритм уточнения для исчисления (ко)индуктивных конструкций» Логические методы в информатике, т. 8, № 1
  5. ^ Андреа Асперти, Уилмер Риччиотти, К. Сакердоти Коэн, Энрико Тасси. «Намеки на унификацию»: LNCS V.5674, 2009, стр. 84-98.
  6. ^ Клаудио Сакердоти Коэн, Стефано Закчироли «Эффективный неоднозначный анализ математических формул» LNCS V.3119, 2004, стр. 347-362
  7. ^ Клаудио Сакердоти Коэн, Энрико Тасси, Стефано Закчироли «Tinycals: Step by Step Tacticals» ENTCS V.174, № 2, 2007, страницы 125–142
  8. ^ Андреа Асперти, Уилмер Риччиотти, Клаудио Сакердоти Коэн «Учебник по Матите» Журнал формализованного рассуждения, т.7, н. 2, 2014, страницы 91–199

Внешние ссылки