Моделирование ограничений Логические программы (для анализа)

Question

Объектно-ориентированные программы могут быть смоделированы различными моделями, такими как Automata, Process Algebras, Petri Nets или UML. Некоторые из этих моделей могут использоваться для выполнения различных видов анализа, чтобы выявить проблемы в производительности или дизайне.

Я изучаю логическое программирование и задаюсь вопросом, существуют ли такие модели для CLP? Как вы проводите анализ программ CLP?

Answer 1

Наиболее подходящими из двух подходов, которые я видел, являются abstract interpretation и evolving algbras (aka Abstract State Machines). Egon Boerger опубликовал формальное определение Пролога и правильное доказательство Уорренской абстрактной машины с использованием эволюционирующих алгебр. Чистые логические языки программирования можно просто моделировать непосредственно в логике.

Answer 2

Обязательно не пропустите cTI_lt (constraint based termination inference for left termination)!

Прекращение вывода - это обобщение без аннотации анализа/проверки завершения. Он смещает фокус программиста от конкретных случаев ко всему отношению. Традиционно анализатор завершения пытается доказать, что заданный класс запросов завершается. Этот класс должен быть предоставлен пользователем, что довольно громоздко, если программы были написаны ранее без каких-либо аннотаций. С завершением вывода никаких аннотаций не требуется. Все доказуемо завершающие классы ко всем связанным предикатам выводятся сразу, иллюстрируя «многонаправленность» предикатов. Это означает, что предикаты можно безопасно использовать в нескольких «направлениях».