Abstract
We present a framework for the declarative diagnosis of non-deterministic timed concurrent constraint programs. We present a denotational semantics based on a (continuous) immediate consequence operator, \(T_{{\mathcal{D}}}\), which models the process behaviour associated with a program \({\mathcal{D}}\) given in terms of sequences of constraints. Then, we show that, given the intended specification of \({\mathcal{D}}\), it is possible to check the correctness of \({\mathcal{D}}\) by a single step of \(T_{{\mathcal{D}}}\). In order to develop an effective debugging method, we approximate the denotational semantics of \({\mathcal{D}}\). We formalize this method by abstract interpretation techniques, and we derive a finitely terminating abstract diagnosis method, which can be used statically. We define an abstract domain which allows us to approximate the infinite sequences by a finite ‘cut’. As a further development we show how to use a specific linear temporal logic for deriving automatically the debugging sequences. Our debugging framework does not require the user to either provide error symptoms in advance or answer questions concerning program correctness. Our method is compositional, that may allow to master the complexity of the debugging methodology.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Alpuente, M., Comini, M., Escobar, S., Falaschi, M., Lucas, S.: Abstract Diagnosis of Functional Programs. In: Leuschel, M.A. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 1–16. Springer, Heidelberg (2003)
Alpuente, M., Correa, F., Falaschi, M.: A Debugging Scheme for Functional Logic Programs. In: Hanus, M. (ed.) Proc. of WFLP 2001. ENTCS, vol. 64, Elsevier, Amsterdam (2002)
Antoy, S., Johnson, S.: TeaBag: A Functional Logic Debugger. In: Kuchen, H. (ed.) Proc. of WFLP 2004, pp. 4–18 (2004)
Bueno, F., Deransart, P., Drabent, W., Ferrand, G., Hermenegildo, M., Maluszyński, J., Puebla, G.: On the role of semantic approximations in validation and diagnosis of constraint logic programs. In: Proc. of AADEBUG 1997, U. of Linkoping Press, pp. 155–170 (1997)
Cameron, M., de la Banda, M.G., Marriott, K., Moulder, P.: Vimer: a visual debugger for mercury. In: Proc. of the 5th PPDP, pp. 56–66. ACM Press, New York (2003)
Comini, M., Gori, R., Levi, G.: Assertion based Inductive Verification Methods for Logic Programs. In: Seda, A.K. (ed.) Proceedings of MFCSIT 2000. ENTCS, vol. 40, Elsevier Science Publishers, Amsterdam (2001)
Comini, M., Levi, G., Meo, M.C., Vitiello, G.: Proving properties of Logic Programs by Abstract Diagnosis. In: Dam, M. (ed.) Analysis and Verification of Multiple-Agent Languages. LNCS, vol. 1192, pp. 22–50. Springer, Heidelberg (1997)
Comini, M., Levi, G., Meo, M.C., Vitiello, G.: Abstract diagnosis. Journal of Logic Programming 39(1-3), 43–93 (1999)
de Boer, F.S., Gabbrielli, M., Marchiori, E., Palamidessi, C.: Proving concurrent constraint programs correct. ACM TOPLAS 19(5), 685–725 (1997)
Ferrand, G.: Error Diagnosis in Logic Programming, an Adaptation of E.Y.Shapiro’s Method. Journal of Logic Programming 4(3), 177–198 (1987)
Hanus, M., Josephs, B.: A debugging model for functional logic programs. In: Penjam, J., Bruynooghe, M. (eds.) PLILP 1993. LNCS, vol. 714, pp. 28–43. Springer, Heidelberg (1993)
Hanus, M., Koj, J.: An integrated development environment for declarative multi-paradigm programming. In: Proc. of the International Workshop on Logic Programming Environments (WLPE 2001), Paphos (Cyprus), pp. 1–14 (2001)
Lloyd, J.W.: Declarative error diagnosis. New Generation Computing 5(2), 133–154 (1987)
Naish, L., Barbour, T.: Towards a portable lazy functional declarative debugger. Australian Computer Science Communications 18(1), 401–408 (1996)
Nielsen, M., Palamidessi, C., Valencia, F.D.: Temporal concurrent constraint programming: Denotation, logic and applications. Nordic Journal of Computing 9(1), 145–188 (2002)
Olarte, C., Rueda, C.: A Stochastic Concurrent Constraint Based Framework to Model and Verify Biological Systems. Clei Electronic Journal 9(2) (2005)
Saraswat, V., Jagadeesan, R., Gupta, V.: Foundations of timed concurrent constraint programming. In: Proc. of the Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 71–80. IEEE Computer Society Press, Los Alamitos (1994)
Saraswat, V.A.: Semantic Foundation of Concurrent Constraint Programming. In: Proc. of 18th ACM POPL, ACM, New York (1991)
Shaphiro, E.Y.: Algorithmic Program Debugging. In: ACM Distinguished Dissertation, The MIT Press, Cambridge, Massachusetts (1982)
Tamaki, H., Sato, T.: Unfold/Fold Transformations of Logic Programs. In: Tärnlund, S. (ed.) Proc. of 2nd ICLP, pp. 127–139 (1984)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Falaschi, M., Olarte, C., Palamidessi, C., Valencia, F. (2007). Declarative Diagnosis of Temporal Concurrent Constraint Programs. In: Dahl, V., Niemelä, I. (eds) Logic Programming. ICLP 2007. Lecture Notes in Computer Science, vol 4670. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74610-2_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-74610-2_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74608-9
Online ISBN: 978-3-540-74610-2
eBook Packages: Computer ScienceComputer Science (R0)