建模約束邏輯程序（用於分析）

Question

面向對象的程序可以用不同的模型建模，例如自動機，進程代數，Petri網或UML。其中一些模型可用於執行各種分析，以發現性能或設計中的問題。

我在研究邏輯編程，想知道是否有這樣的CLP模型？你如何分析CLP計劃？

Answer 1

我見過的兩種方法使用最多的是abstract interpretation和evolving algbras（又名抽象狀態機）。 Egon Boerger發表了Prolog的正式定義和使用演化代數的Warren抽象機的correctnes證明。純邏輯編程語言可以直接在邏輯中建模。

Answer 2

千萬不要錯過cTI_lt (constraint based termination inference for left termination)！

終止推斷是終止分析/檢查的免註釋概括。它將程序員的注意力從特定情況轉移到整個關係。傳統上，終端分析器試圖證明給定的一類查詢終止。這個類必須由用戶提供，如果程序以前沒有任何註釋，那麼這很麻煩。通過終止推理，不需要註釋。所有相關謂詞的所有可證明的終止類都被立即推斷出來，說明謂詞的「多方向性」。這意味着謂詞可以在幾個'方向'上安全地使用。