Illustriamo qui brevemente la nostra esperienza nel campo della verifica e delle trasformazioni dei programmi logici. Pur occupandoci ora di tematiche completamente diverse, verifica di proprieta` di sicurezza da un lato e analisi di sistemi biologici dall’altro, continuiamo ad utilizzare proficuamente la nostra precedente esperienza. In this paper, we briefly describe our esperience in the field of verification and transformation of logic programming. Though now we are working in a completely different field, verification of security properties on one hand and biosystems analysis on the other, our previous experience continues to be a valuable guide.
Keywords: logic programming, termination verification, program transformation 1
It is very pleasant to remember the time we spent in working on Logic Programming. The friendship and warmth of the people we met, the enthusiasm and interest in research, the curiosity and joy of young researchers, have been strong reasons for working in this field and to be happy with it.
Our main interest, since the beginning, was analysis and verification of logic programs and program transformation. After more than fifteen years of happy and satisfactory research, we felt the need to enlarge our research field and we tried to export our expertise in Computational Logic to different research topics.
In the following section we briefly resume our main results in the field of logic programming and then we give a brief account of our present research interests.
Programming methodology imposes to focus first on the correctness of a program and only later on its efficiency. This is necessary also in logic programming and it requires both program verification and program optimization tools. Our research in LP has been motivated by these needs, dealing mainly with transformation systems and with analysis techniques.
Analysis techniques.
Logic programs are declarative in essence, and this is a
great advantage for programs prototyping and
development. Nevertheless, there are properties which are not
directly expressed by the program itself and have to be
proved. We proposed a technique for verifying
correctness and completeness of a logic program with respect to
a Pre/Post declarative specification of data properties [
Techniques for verifying termination.
Termination is an essential property of programs. We considered the problem of verifying universal termination of logic programs. This is a rather strong requirement for a query, namely to have only finite LD-derivations1. All the methods to solve this problem, if effective, can only provide sufficient criteria for termination. In our works we developed various methods for the analysis of universal termination by considering different classes of programs which can be verified.
We introduced a class of functions to weight the terms
occurring in a program (semilinear norms) [
In [
Trasformations on logic and Prolog programs. Program transformations are applied both in program synthesis and in program optimization. For logic programs the “logic” component makes transformations very natural and easy to be studied formally. But, when we move to Prolog programs, non-declarative properties, like termination, cannot be ignored.
At first we focused on program specialization, which
consists in restricting the applicability of the original
program while optimizing it: the specialized program deals
with fewer cases but in a more efficient way. Some parts
of the computation become redundant, other parts can be
pre-computed (partial evaluation). Specialization seems to
fit very well logic programs in order to pass from a
relational definition to some specific functionalities. We
proposed a methodology for specializing a logic program [
- new definition, it defines a new predicate in terms of other predicates already available in the program; - unfold, it substitutes an atom in a clause body with all its definitions;
- fold, it substitutes a set of atoms in a clause body with an equivalent atom; - prune, it removes a redundant clause from the program; - thin, it removes a redundant literal from a clause body; - fatten, it adds further literals in a clause body whenever this allows for simplifications;
- replace, it substitutes a set of literals in a clause body for another set of literals; it is a generalization of the thin and fatten operations.
Each operation must produce a program which is
equivalent to the original one, but more efficient. Program
equivalence depends on the semantics we consider. Hence,
we studied these transformation operations with respect to
different program semantics. Our effort has been to
determine sufficient conditions, simple to verify, for the
various operations and semantics. We considered the classic
semantics given by the minimal Herbrand model [
Besides basic transformation operations, we defined
simultaneous replacement and we studies it with respect to
the three-valued completion of a logic program [
Any transformation system is a source-to-source rewriting methodology devised to improve the efficiency of a program. Any such transformation should preserve the main properties of the initial program. The transformation operations defined for logic programs do not consider operational properties, among them, termination. These properties become relevant for Prolog programs. To deal with that we followed two approaches.
On one hand, we considered acyclic programs, namely
programs which terminate for each ground query and any
selection rule, and acceptable programs, namely programs
which terminate for each ground query and leftmost
selection rule. For both of them we identified the subclasses of
programs closed under unfold and fold operations [
In order to be applicable most of the transformations
require to reorder the atoms in clause bodies, then in [
On the other hand, in [
In [
Our work on the semantics of logic programming is ruled
by the convincement that a semantics should help in
understanding the meaning of programs by providing
useful notions of observable program equivalences. The
ssemantic approach (see [
Most logic programming languages offer some kind
of dynamic scheduling to increase the expressive power
and to control execution. But the presence of dynamic
scheduling makes more complex the programs behaviour
and more difficult the description of the semantics. Input
consuming derivations have been introduced and studied
in [
Verification of security properties.
In the recent years, security has gained more and more importance. In this field, our research focus on information flow properties, i.e., security properties that allow one to express constraints on how information should flow among different groups of entities. An interesting feature of these kind of properties, is that they protect the system even against internal attacks performed by, e.g., viruses or Trojan horses.
We study different classes of security properties and
conditions to ensure global properties by means of local
unwinding conditions [
For many practical applications the requirement of
a complete absence of any information flow could be
stronger than necessary when some knowledge about the
environment (context) in which the process is going to run
is available. To relax this requirement we introduce a
general notion of secure contexts for a process [
Biosystems analysis.
Computational biology is a recent field combining computer science and molecular biology to study living beings. We focus our attention on two areas, pattern discovery and system biology.
Pattern discovery. Many biological problems require to
blindly search into DNA or protein sequences for
relevant signals. Often we may assume that strings which
appears ”strangely often” or ”strangely rarely” in such
sequences have an associated functional purpose. We
studied the techniques for finding such signals and for giving
them a compact representation as patterns. In particular
we define maximal patterns [
Our thanks to Matteo Baldoni and Cristina Baroglio for organizing this collection in honour of Alberto Martelli, a dear friend and one of the most attracting personality for the Italian Computational Logic community.