Моделирование программ логики ограничений (для анализа)
Объектно-ориентированные программы могут моделироваться различными моделями, такими как Автоматы, Алгебры Процессов, Сети Петри или UML. Некоторые из этих моделей могут использоваться для выполнения различного вида анализа, чтобы выявить проблему в производительности или дизайне.
Я изучаю логическое программирование и спрашиваю себя, есть ли такие модели для CLP? Как вы делаете анализ программ CLP?
2 ответа
Два подхода, которые я видел, использовали больше всего, это абстрактная интерпретация и эволюционирующие алгебры (или абстрактные автоматы). Эгон Бургер опубликовал формальное определение Пролога и корректное доказательство абстрактной машины Уоррена с использованием эволюционирующих алгебр. Чисто логические языки программирования могут быть смоделированы непосредственно в логике.
Убедитесь, что не пропустили cTI_lt (основанный на ограничении вывод завершения для левого завершения)!
Вывод о завершении - это обобщение без анализа аннотации / проверки завершения. Это смещает внимание программиста с отдельных случаев на все отношение. Традиционно анализатор завершения пытается доказать, что данный класс запросов завершается. Этот класс должен быть предоставлен пользователем, что довольно громоздко, если программы были написаны ранее без каких-либо аннотаций. С выводом завершения аннотации не нужны. Все доказуемо завершающие классы для всех связанных предикатов выводятся одновременно, иллюстрируя "разнонаправленность" предикатов. Это означает, что предикаты могут безопасно использоваться в нескольких "направлениях".