Кодируется ли процесс доказательства с помощью средства доказательства теорем Изабель в режиме программирования, а затем проверяется в режиме доказательства?

Question

Мой вопрос касается процесса доказательства механизма доказательства теорем Изабель.

В настоящее время меня интересует исследовательская работа по корректности преобразований моделей . Однако при формализации языка моделирования возникли проблемы. Для формального языка моделирования (включая исходную метамодель, целевую метамодель, само преобразование), но он не уверен в механизме доказательства теоремы .

Должен ли я сам -кодировать файл теории с суффиксом .thy в режиме программирования, а затем запустить его в режиме проверки, чтобы получить подтверждение правильности? У Изабель есть много полей для кодирования, таких как типы данных, константы, функции, определения, леммы и теоремы. Следует ли закодировать их отдельно , чтобы доказать правильность преобразований модели?

Answer 1

Я не уверен, что правильно понял ваш вопрос, но я постараюсь ответить на него частично.

Однако при формализации языка моделирования возникли проблемы.

Не могли бы вы пояснить, с какими проблемами вы столкнулись, или привести конкретный пример языка моделирования, который вы хотите формализовать?

Следует ли мне самокодировать файл теории с суффиксом .thy в режиме программирования, а затем запустить его в режиме проверки, чтобы получить подтверждение правильности?

У Изабель нет отдельных режимов для программирования и для проверки. Вы можете смешивать определения функций и леммы в одном файле .thy.

Большинство аспектов корректности отражено в леммах / теоремах, но даже если вы просто определите рекурсивную функцию в Isabelle, вы уже получите некоторые гарантии корректности : вам нужно доказать, что ваше определение четко определено.

Изабель имеет множество полей кодирования, таких как типы данных, константы, функции, определения, леммы и теоремы. Следует ли кодировать их отдельно, чтобы доказать правильность преобразований модели?

Как я сказал выше, вам не нужно разделять их на разные файлы. Однако в Изабель все должно быть определено по порядку. Например, если вы хотите что-то доказать о функции, тогда функция должна быть определена до леммы в исходном коде. Если функция работает с некоторой структурой данных, соответствующие определения типа должны быть перед функцией.