=Paper=
{{Paper
|id=Vol-487/paper-12
|storemode=property
|title=A Valuable Experience in Computational Logic
|pdfUrl=https://ceur-ws.org/Vol-487/paper12.pdf
|volume=Vol-487
|dblpUrl=https://dblp.org/rec/conf/birthday/BossiC08
}}
==A Valuable Experience in Computational Logic==
https://ceur-ws.org/Vol-487/paper12.pdf
Il Milione: A Journey in the Computational Logic in Italy
Una fruttuosa esperienza in Logica Computazionale
A valuable experience in Computational Logic
Annalisa Bossi, Nicoletta Cocco
Dipartimento di Informatica, Università Ca’ Foscari di Venezia,
via Torino 155, 30172, Venezia, Italy
email: {bossi, cocco}@dsi.unive.it
65
Il Milione: A Journey in the Computational Logic in Italy
SOMMARIO/ABSTRACT 2 Our contribution to Logic Programming
Programming methodology imposes to focus first on the
Illustriamo qui brevemente la nostra esperienza nel campo
correctness of a program and only later on its efficiency.
della verifica e delle trasformazioni dei programmi logici.
This is necessary also in logic programming and it requires
Pur occupandoci ora di tematiche completamente diverse,
both program verification and program optimization tools.
verifica di proprietà di sicurezza da un lato e analisi di
Our research in LP has been motivated by these needs,
sistemi biologici dall’altro, continuiamo ad utilizzare
dealing mainly with transformation systems and with anal-
proficuamente la nostra precedente esperienza.
ysis techniques.
Analysis techniques.
In this paper, we briefly describe our esperience in the field Logic programs are declarative in essence, and this is a
of verification and transformation of logic programming. great advantage for programs prototyping and develop-
Though now we are working in a completely different field, ment. Nevertheless, there are properties which are not
verification of security properties on one hand and biosys- directly expressed by the program itself and have to be
tems analysis on the other, our previous experience contin- proved. We proposed a technique for verifying correct-
ues to be a valuable guide. ness and completeness of a logic program with respect to
a Pre/Post declarative specification of data properties [1].
Keywords: logic programming, termination verification, This can be used to guarantee both the correspondence of
program transformation the program to its intended meaning and the applicabil-
ity of program transformations. We considered also the
operational property on having successes, or finite fail-
ures, which is relevant for query correctness and efficiency
1 Introduction [5, 6]. Besides, the property of not having finite failures
can be used to simplify applicability conditions of program
It is very pleasant to remember the time we spent in work- transformation operations.
ing on Logic Programming. The friendship and warmth Techniques for verifying termination.
of the people we met, the enthusiasm and interest in re- Termination is an essential property of programs. We con-
search, the curiosity and joy of young researchers, have sidered the problem of verifying universal termination of
been strong reasons for working in this field and to be logic programs. This is a rather strong requirement for a
happy with it. query, namely to have only finite LD-derivations1 . All the
Our main interest, since the beginning, was analysis and methods to solve this problem, if effective, can only pro-
verification of logic programs and program transformation. vide sufficient criteria for termination. In our works we
After more than fifteen years of happy and satisfactory re- developed various methods for the analysis of universal
search, we felt the need to enlarge our research field and termination by considering different classes of programs
we tried to export our expertise in Computational Logic to which can be verified.
different research topics. We introduced a class of functions to weight the terms
occurring in a program (semilinear norms) [16, 18]. The
In the following section we briefly resume our main re-
norms in this class provide a syntactical characterization
sults in the field of logic programming and then we give a
brief account of our present research interests. 1 SLD-derivations build with the leftmost selection rule.
66
Il Milione: A Journey in the Computational Logic in Italy
of rigid terms, i.e. terms whose weight does not change this allows for simplifications;
under substitution. The notion of rigid term generalizes - replace, it substitutes a set of literals in a clause body
the notion of ground term. We defined a proof method for for another set of literals; it is a generalization of the thin
universal termination, based on Pre/Post conditions which and fatten operations.
deal with the rigidity of terms and can be derived by the Each operation must produce a program which is equiv-
mode and type properties of atoms. In [17] we general- alent to the original one, but more efficient. Program
ized our previous work by considering also terms with a equivalence depends on the semantics we consider. Hence,
specified structure by means of typed norms. Besides, we we studied these transformation operations with respect to
studied how mode and type information can be used for different program semantics. Our effort has been to deter-
characterizing termination properties. We defined the class mine sufficient conditions, simple to verify, for the vari-
of well-moded programs [31], namely programs which ous operations and semantics. We considered the classic
are inductively ”well-formed” with respect to a specified semantics given by the minimal Herbrand model [7] and
input-output functionality. This allowed us to define and the semantics given by computed answers substitutions [2].
characterize well-terminating programs, namely programs Moreover, in [8, 9] we considered general programs (with
for which all well-moded queries have only finite LD- negation) and some semantics for them, such as Fitting’s
derivations. We proposed also a termination property for semantics, Kunen’s semantics, and the Well-founded se-
general logic programs (programs with negation) [19]. A mantics.
general program is typed-terminating if it terminates for Besides basic transformation operations, we defined si-
any well-typed query. These definitions lead to sufficient multaneous replacement and we studies it with respect to
conditions for termination which are compositional and the three-valued completion of a logic program [11].
simple to verify. Any transformation system is a source-to-source rewrit-
In [14] we completed our work on the verification of ter- ing methodology devised to improve the efficiency of a
mination properties, by proposing a modular proof tech- program. Any such transformation should preserve the
nique applicable to hierarchical general programs. Be- main properties of the initial program. The transforma-
sides, by using mode or type information, it is possible to tion operations defined for logic programs do not consider
verify termination incrementally. operational properties, among them, termination. These
Trasformations on logic and Prolog programs. properties become relevant for Prolog programs. To deal
Program transformations are applied both in program syn- with that we followed two approaches.
thesis and in program optimization. For logic programs On one hand, we considered acyclic programs, namely
the “logic” component makes transformations very natural programs which terminate for each ground query and any
and easy to be studied formally. But, when we move to selection rule, and acceptable programs, namely programs
Prolog programs, non-declarative properties, like termina- which terminate for each ground query and leftmost selec-
tion, cannot be ignored. tion rule. For both of them we identified the subclasses of
At first we focused on program specialization, which programs closed under unfold and fold operations [20, 11].
consists in restricting the applicability of the original pro- In order to be applicable most of the transformations re-
gram while optimizing it: the specialized program deals quire to reorder the atoms in clause bodies, then in [12] we
with fewer cases but in a more efficient way. Some parts extended the previous work by considering also a switch
of the computation become redundant, other parts can be operation which allows one to reorder consecutive atoms.
pre-computed (partial evaluation). Specialization seems to On the other hand, in [3, 4] we followed a more opera-
fit very well logic programs in order to pass from a rela- tional approach and we defined a non-increasing property
tional definition to some specific functionalities. We pro- for a transformation. It is a very strong property which
posed a methodology for specializing a logic program [7] guarantees that the transformation is both preserving uni-
and studied a set of basic transformation operations which versal termination and optimizing, since it cannot increase
allow one (i) to associate a new application domain to the the depth of the derivation tree associated to a query.
query by means of constraints, and (ii) to propagate them In [13] we considered and analyzed the main systems for
through the program for optimizing it. The set of basic transforming logic and Prolog programs. In particular we
operations includes: discuss if they preserve non-declarative properties of the
- new definition, it defines a new predicate in terms of original program and specifically termination properties.
other predicates already available in the program; Semantics for logic programs.
- unfold, it substitutes an atom in a clause body with all Our work on the semantics of logic programming is ruled
its definitions; by the convincement that a semantics should help in un-
- fold, it substitutes a set of atoms in a clause body with derstanding the meaning of programs by providing use-
an equivalent atom; ful notions of observable program equivalences. The s-
- prune, it removes a redundant clause from the program; semantic approach (see [26]) provides a methodology to
- thin, it removes a redundant literal from a clause body; define semantics which enjoy this property. Each seman-
- fatten, it adds further literals in a clause body whenever tics in the approach captures some observable properties
67
Il Milione: A Journey in the Computational Logic in Italy
of logic programs and allows us to detect when two pro- vant signals. Often we may assume that strings which ap-
grams are undistinguishable by observing their behaviors, pears ”strangely often” or ”strangely rarely” in such se-
thus providing a suitable base for program analysis and quences have an associated functional purpose. We stud-
transformation. Following this approach, we defined the ied the techniques for finding such signals and for giving
Ω- semantics, a compositional semantics for positive logic them a compact representation as patterns. In particular
programs. It provides a refined notion of observational we define maximal patterns [30], which correspond to the
equivalence which takes into account both computed an- largest subsets of strings which can be grouped together.
swers and program composition by union of clauses [27]. The set of maximal patterns is unique and very readable,
Most logic programming languages offer some kind intuitively it represents all possible ”most abstract views”
of dynamic scheduling to increase the expressive power of the strings we are interested in. We propose two differ-
and to control execution. But the presence of dynamic ent algorithms for computing the set of maximal patterns.
scheduling makes more complex the programs behaviour Systems biology is a rather new field studying complex in-
and more difficult the description of the semantics. Input teractions in biological systems. The aim is to model such
consuming derivations have been introduced and studied systems, to formally analyze their properties and to sim-
in [21, 22, 23] to describe dynamic scheduling while ab- ulate their behaviour. This would make possible to do in
stracting from the technical details. In [15] we reviewed silico experiments instead of in vivo experiments, which
and compared the different proposals given for dynamic may be difficult, or even impossible, to perform on biolog-
scheduling and in particular for the denotational semantics ical systems. Computational logic and formal techniques
of programs with input consuming derivations. We also to specify and analyze concurrent processes can be applied
show how they can be applied to termination analysis. to this field.
3 Present Research 4 Acknowledgements
Verification of security properties. Our thanks to Matteo Baldoni and Cristina Baroglio for
In the recent years, security has gained more and more im- organizing this collection in honour of Alberto Martelli, a
portance. In this field, our research focus on information dear friend and one of the most attracting personality for
flow properties, i.e., security properties that allow one to the Italian Computational Logic community.
express constraints on how information should flow among
different groups of entities. An interesting feature of these REFERENCES
kind of properties, is that they protect the system even
against internal attacks performed by, e.g., viruses or Tro- [1] A. Bossi and N. Cocco. Verifying Correctness of Logic
jan horses. Programs. In J. Diaz and F. Orejas, editors, Proceed-
We study different classes of security properties and ings TAPSOFT ’89, Barcelona, Spain, LNCS 352, pp.
conditions to ensure global properties by means of local 96–110, Springer-Verlag, 1989.
unwinding conditions [25]. Locality allows us to define a
proof system which provides a very efficient technique for [2] A. Bossi, e N. Cocco. Basic Transformation Opera-
the development and verification of secure processes [24]. tions which preserve Computed Answer Substitutions
For many practical applications the requirement of of Logic Programs. Journal of Logic Programming,
a complete absence of any information flow could be 16:47–87, 1993.
stronger than necessary when some knowledge about the
environment (context) in which the process is going to run [3] A. Bossi and N. Cocco. Preserving universal ter-
is available. To relax this requirement we introduce a gen- mination through unfold/fold. In G. Levi and
eral notion of secure contexts for a process [28]. In [29] M. Rodrı́guez-Artalejo, editors, Proceedings ALP’94,
we moved from a process algebra setting to a standard LNCS 850, pp. 269–286, Springer-Verlag, 1994.
programming environment. We present a general unwind-
[4] A. Bossi and N. Cocco. Replacement Can Pre-
ing framework for the definition of information flow secu-
serve Termination. In J. Gallagher, editor, Proceed-
rity properties of concurrent programs, described in a stan-
ings LOPSTR’96, LNCS 1207, pp.104–129, Springer-
dard imperative language, admitting parallel executions on
Verlag, 1997.
a shared memory.
Biosystems analysis. [5] A. Bossi and N. Cocco. Programs without Failures.
Computational biology is a recent field combining com- In N. Fuchs, editor, Proceedings LOPSTR’97, LNCS
puter science and molecular biology to study living beings. 1463, pp. 28–48, Springer-Verlag,1998.
We focus our attention on two areas, pattern discovery and
system biology. [6] A. Bossi and N. Cocco. Successes in Logic Programs.
Pattern discovery. Many biological problems require to In P. Flener, editor, Proceedings LOPSTR’98, LNCS
blindly search into DNA or protein sequences for rele- 1559, pp. 219–239, Springer-Verlag, 1999.
68
Il Milione: A Journey in the Computational Logic in Italy
[7] A. Bossi, N. Cocco, e S. Dulli. A Method for Spe- [18] A. Bossi, N. Cocco, and M. Fabris. Norms on
cializing Logic Programs. ACM Transactions on Pro- terms and their use in proving universal termination
gramming Languages and Systems, 12(2):253–302, of a logic program. Theoretical Computer Science,
1990. 124:297–328, 1994.
[8] A. Bossi, N. Cocco, e S. Etalle. On Safe Folding. In [19] A. Bossi, N. Cocco, and S. Rossi. Termination of
M. Bruynooghe and M. Wirsing, editors, Proceedings Well-Typed Logic Programs. In H. Sondergaard editor,
PLILP’92, Leuven, Belgium, LNCS 631, pp. 172–186, Proceedings PPDP’01, Firenze, Italy, pp.73-81, ACM
Springer-Verlag, 1992. Press, 2001.
[20] A. Bossi and S. Etalle. Transforming Acyclic Pro-
[9] A. Bossi, N. Cocco, e S. Etalle. Transforming Normal grams. ACM Transactions on Programming Lan-
Programs by Replacement. In A. Pettorossi, editor, guages and Systems, 16(4):1081–1096, July 1994.
Proceedings META’92, Uppsala, Sweden, LNCS 649,
pp. 265–279, Springer-Verlag, 1992. [21] A. Bossi, S. Etalle, and S. Rossi. Semantics of well-
moded input-consuming logic programs. Computer
[10] A. Bossi, N. Cocco, and S. Etalle. Transformation of Languages, 26(1):1–25, 2000.
Left Terminating Programs: the Reordering Problem.
[22] A. Bossi, S. Etalle, and S. Rossi. Properties of input-
In M. Proietti, editor, Proceedings LOPSTR’95, LNCS
consuming derivations. Theory and Practice of Logic
1048, pp. 33–45, Springer-Verlag, 1995.
Programming, 2(2):125–154, 2002.
[11] A. Bossi, N. Cocco, e S. Etalle. Simultaneous Re- [23] A. Bossi, S. Etalle, S. Rossi, and J.-G. Smaus. Ter-
placement in Normal Programs. Journal of Logic and mination of simply-moded logic programs with dy-
Computation, 6(1):79–120, 1996. namic scheduling. ACM Transactions on Computa-
tional Logic (TOCL), 5(3):470–507, 2004.
[12] A. Bossi, N. Cocco, e S. Etalle. Transformation of
Left Terminating Programs. In A. Bossi editor, Pro- [24] A. Bossi, R. Focardi, C. Piazza, and S. Rossi. A proof
ceedings of LOPSTR’99, Venezia, Italy, LNCS 1817, system for information flow security. M. Leuschel, ed-
pp. 156-175, Springer-Verlag, 2000. itor, Proceedings LOPSTR’02, LNCS 2664, pp. 2199–
218, Springer-Verlag, 2003.
[13] A. Bossi, N. Cocco e S. Etalle. Transformation Sys-
tems and Nondeclarative Properties. In A. Kakas and [25] A. Bossi, R. Focardi, C. Piazza, and S. Rossi.
F. Sadri editors, Computational Logic: Logic Pro- Verifying persistent security properties. Computer
gramming and Beyond (Essays in honour of Robert A. Languages, Systems and Structures, 30(3-4):231–258,
Kowalski). LNAI 2407, pp. 162-186, Springer-Verlag, 2004.
2002. [26] A. Bossi, M. Gabrielli, G. Levi, and M. Martelli.
The S-semantics approach: Theory and applications.
[14] A. Bossi, S. Etalle N. Cocco, and S. Rossi. On Mod- The Journal of Logic Programming, 19 & 20:149–198,
ular Termination Proofs of General Logic Programs. May 1994.
Theory and Practice of Logic Programming, 2(3):263–
291, 2002. [27] A. Bossi, M. Gabbrielli, G. Levi, and M. C. Meo. A
compositional semantics for logic programs. Theoret-
[15] A. Bossi, S. Etalle N. Cocco, and S. Rossi. Declar- ical Computer Science, 122(1-2):3–47, 1994.
ative Semantics of Input-Consuming Logic Programs.
[28] A. Bossi, D. Macedonio, C. Piazza, and S. Rossi. In-
In M. Bruynooghe, K. Lau editors, Program Devel-
formation flow in secure contexts. Journal of Com-
opment in Computational Logic - A Decade of Re-
puter Security, 13(3):391–422, 2005.
search Advances in Logic-Based Program Develop-
ment. LNCS 3049, Springer-Verlag, 2004. [29] A. Bossi, C. Piazza, and S. Rossi. Compositional in-
formation flow security for concurrent programs. Jour-
[16] A. Bossi, N. Cocco, and M. Fabris. Proving termina- nal of Computer Security, 15(3):373–413, 2007.
tion of logic programs by exploiting term properties.
In S. Abramsky and T.S.E. Maibaum, editors, Pro- [30] N. Cocco and M. Simeoni, Maximal abstraction of
ceedings CCPSD-TAPSOFT’91, LNCS 494, pp. 153– strings. Dipartimento di Informatica, Università Ca’
180, Springer-Verlag, 1991. Foscari di Venezia, Rapporto di ricerca CS-2007-2,
2007.
[17] A. Bossi, N. Cocco, and M. Fabris. Typed Norms. [31] S. Etalle, A. Bossi, and N. Cocco. Termination of
In Krieg-Bruckner, editor, Proceedings ESOP’92, well-moded programs. Journal of Logic Program-
Rennes, France, LNCS 582, pp. 73–92. Springer- ming, 38(2):243–257, 1999.
Verlag, 1992.
69