Selective Unification in (Constraint) Logic Programming

• Autorzy: Mesnard Fred , Payet Étienne , Vidal Germán

Identyfikatory

DOI

10.3233/FI-2020-1993

• Języki publikacji: EN

Abstrakty

EN

Concolic testing is a well-known validation technique for imperative and object oriented programs. In a previous paper, we have introduced an adaptation of this technique to logic programming. At the heart of our framework lies a specific procedure that we call “selective unification”. It is used to generate appropriate run-time goals by considering all possible ways an atom can unify with the heads of some program clauses. In this paper, we show that the existing algorithm for selective unification is not complete in the presence of non-linear atoms. We then prove soundness and completeness for a restricted version of the problem where some atoms are required to be linear. We also consider concolic testing in the context of constraint logic programming and extend the notion of selective unification accordingly.

Słowa kluczowe

EN

logic programming; constraint logic programming; concolic testing; unification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 177, nr 3/4
• Strony: 359--383
• Opis fizyczny: Bibliogr. 16 poz.

Twórcy

autor

Mesnard Fred

• LIM - Université de la Réunion, Réunion, France

autor

Payet Étienne

• LIM - Université de la Réunion, Réunion, France

autor

Vidal Germán

• MiST, VRAIN, Universitat Politècnica de València, València, Spain

Bibliografia

• [1] Mesnard F, Payet E, Vidal G. Concolic Testing in Logic Programming. Theory and Practice of Logic Programming, 2015. 15(4-5):711-725. doi:10.1017/S1471068415000332.
• [2] Jaffar J, Lassez JL. Constraint Logic Programming. In: Proc. of the 14th Annual ACM Symposium on Principles of Programming Languages (POPL’87). ACM Press, 1987 pp. 111-119. doi:10.1145/41625.41635.
• [3] Jaffar J, Maher MJ. Constraint Logic Programming: A Survey. Journal of Logic Programming, 1994. 19,20:503-581. doi:10.1016/0743-1066(94)90033-7.
• [4] Apt KR. From Logic Programming to Prolog. Prentice Hall, 1997. ISBN 978-0-13-230368-2.
• [5] Jaffar J, Maher MJ, Marriott K, Stuckey PJ. The Semantics of Constraint Logic Programs. Journal of Logic Programming, 1998. 37(1-3):1-46. doi:10.1016/S0743-1066(98)10002-X.
• [6] Refalo P, Van Hentenryck P. CLP(Rlin) Revised. In: Maher M (ed.), Proc. of the Joint International Conference and Symposium on Logic Programming. The MIT Press, 1996 pp. 22-36.
• [7] Marriott K, Stuckey PJ. Programming with Constraints: An Introduction. The MIT Press, 1998.
• [8] Ströder T, Emmes F, Schneider-Kamp P, Giesl J, Fuhs C. A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog. In: Vidal G (ed.), Proc. of the 21st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR’11), volume 7225 of Lecture Notes in Computer Science. Springer, 2012 pp. 237-252. doi:10.1007/978-3-642-32211-2_16.
• [9] Palamidessi C. Algebraic Properties of Idempotent Substitutions. In: Paterson MS (ed.), Proc. of the 17th International Colloquium on Automata, Languages and Programming (ICALP’90), volume 443 of Lecture Notes in Computer Science. Springer, 1990 pp. 386-399. doi:10.1007/BFb0032046.
• [10] Mesnard F, Payet E, Vidal G. Selective Unification in Constraint Logic Programming. In: Vanhoof W, Pientka B (eds.), Proc. of the 19th International Symposium on Principles and Practice of Declarative Programming (PPDP’17). ACM, 2017 pp. 115-126. doi:10.1145/3131851.3131863.
• [11] Bradley AR, Manna Z, Sipma HB. What’s Decidable About Arrays? In: Emerson EA, Namjoshi KS (eds.), Proc. of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’06), volume 3855 of Lecture Notes in Computer Science. Springer, 2006 pp. 427-442. doi:10.1007/11609773_28.
• [12] Mesnard F, Payet E, Vidal G. On the Completeness of Selective Unification in Concolic Testing of Logic Programs. In: Hermenegildo MV, López-García P (eds.), Proc. of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR’16), volume 10184 of Lecture Notes in Computer Science. Springer, 2016 pp. 205-221. doi:10.1007/978-3-319-63139-4_12.
• [13] Chan D. Constructive Negation Based on the Completed Database. In: Kowalski RA, Bowen KA (eds.), Proc. of the 5th International Conference and Symposium on Logic Programming (ICLP/SLP’88). MIT Press, 1988 pp. 111-125.
• [14] Stuckey PJ. Negation and Constraint Logic Programming. Information and Computation, 1995. 118(1):12-33. doi:10.1006/inco.1995.1048.
• [15] Dovier A, Pontelli E, Rossi G. A Necessary Condition for Constructive Negation in Constraint Logic Programming. Information Proc. Letters, 2000. 74(3-4):147-156. doi:10.1016/S0020-0190(00)00046-6.
• [16] Fortz S, Mesnard F, Payet E, Perrouin G, Vanhoof W, Vidal G. An SMT-Based Concolic Testing Tool for Logic Programs. Technical report, Universitat Politècnica de València, 2019. Submitted for publication, URL http://personales.upv.es/gvidal/german/SMTConcolicTool/paper.pdf.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).