=Paper=
{{Paper
|id=Vol-487/paper-2
|storemode=property
|title=Program Transformation for Development, Verification, and Synthesis of Software
|pdfUrl=https://ceur-ws.org/Vol-487/paper2.pdf
|volume=Vol-487
|dblpUrl=https://dblp.org/rec/conf/birthday/PettorossiPS08
}}
==Program Transformation for Development, Verification, and Synthesis of Software==
https://ceur-ws.org/Vol-487/paper2.pdf
Il Milione: A Journey in the Computational Logic in Italy
LA TRASFORMAZIONE DEI PROGRAMMI PER LO
SVILUPPO, LA VERIFICA E LA SINTESI DEL SOFTWARE
PROGRAM TRANSFORMATION FOR DEVELOPMENT,
VERIFICATION, AND SYNTHESIS OF SOFTWARE
Alberto Pettorossi, Maurizio Proietti, Valerio Senni
7
Il Milione: A Journey in the Computational Logic in Italy
SOMMARIO/ABSTRACT properties of infinite state systems that cannot be analyzed
by using standard model checking techniques.
In questo articolo presentiamo brevemente la metodologia In what follows we will illustrate the three uses of pro-
di trasformazione dei programmi per lo sviluppo di soft- gram transformation we have mentioned above, namely
ware corretto ed efficiente. Ci riferiremo, in particolare, al (i) program improvement, (ii) program synthesis, and
caso della trasformazione e dello sviluppo dei programmi (iii) program verification. In particular, we will consider
logici con vincoli. the case of algorithms and specifications written as con-
straint logic programs [12] and we will focus our attention
In this paper we briefly describe the use of the program on the following transformation rules [1, 6, 8, 9, 25, 26]:
transformation methodology for the development of cor- definition, unfolding, folding, goal replacement, and clause
rect and efficient programs. We will consider, in particular, splitting which will be applied according to some specific
the case of the transformation and the development of con- strategies. This approach to program transformation is,
straint logic programs. thus, called the rules + strategies approach.
Keywords: Constraint logic programming, model check-
2 Program improvement
ing, program synthesis, unfold/fold program transforma-
tion, software verification. Programs are often written in a parametric form so that
they can be reused in different contexts, and when a para-
1 Introduction metric program is reused, one may want to transform it for
taking advantage of the new context of use. This transfor-
The program transformation methodology has been intro- mation, called program specialization [10, 13, 16], usually
duced in the case of functional programs by Burstall and allows a great efficiency improvement. Let us present an
Darlington [3] and then it has been adapted to logic pro- example of this transformation by deriving a deterministic,
grams by Hogger [11] and Tamaki and Sato [26]. The main specialized pattern matcher from a given nondeterminis-
idea of this methodology is to transform, maybe in sev- tic, parametric pattern matcher and a specific pattern. In
eral steps and by applying different transformation rules, this example the matching relation on strings of numbers
the given initial program into a final program with the aim is the relation le m(P, S) which holds between a pattern
¯
of improving its efficiency and preserving its correctness. P = [p1 , . . . , pn ] and a string S iff in S there exists a sub-
If the initial program is a non-executable specification of string Q = [q1 , . . . , qn ] such that for i = 1, . . . , n, pi ≤ qi .
an algorithm, while the final program is executable, then (This example can be generalized by considering any re-
program transformation is equivalent to program synthe- lation which can be expressed via a constraint logic pro-
sis. Thus, program transformation can be viewed as a tech- gram.)
nique both: (i) for program improvement and advanced The following constraint logic program can be taken as
compilation, and (ii) for program synthesis and program the specification of our general pattern matching problem:
development. 1. le m(P, S) ← ap(B, C, S)∧ap(A, Q, B)∧le(P, Q)
In recent years program transformation has also been ¯
2. ap([ ], Ys, Ys) ←
used as a technique for program verification. It has been 3. ap([X|Xs], Ys, [X|Zs]) ← ap(Xs, Ys, Zs)
shown, in fact, that via program transformation one can 4. le([ ], [ ]) ←
perform model checking and, in general, one can prove 5. le([X|Xs], [Y |Ys]) ← X ≤ Y ∧le(Xs, Y s)
8
Il Milione: A Journey in the Computational Logic in Italy
where ap denotes list concatenation. Suppose that we want 9. le ms (S) ← new 1(S)
¯
to use this general program in the case of the pattern P = 16. new 1([X|Xs]) ← 1 ≤ X∧new 2(Xs)
[1,0,2]. We start off our transformation by introducing the 17. new 1([X|Xs]) ← 1 > X∧new 1(Xs)
following clause by applying the so-called definition rule: 18. new 2([X|Xs]) ← 1 ≤ X∧new 3(Xs)
19. new 2([X|Xs]) ← 0 ≤ X∧1 > X∧new 4(Xs)
6. le ms (S) ← le m([1,0,2], S)
¯ ¯ 20. new 2([X|Xs]) ← 0 > X∧new 1(Xs)
Clauses 1–6 constitute the initial program from which 21. new 3([X|Xs]) ← 2 ≤ X ∧new 5(Xs)
we begin our program transformation process by apply- 22. new 3([X|Xs]) ← 1 ≤ X∧2 > X∧new 3(Xs)
ing the transformation rules according to the so-called De- 23. new 3([X|Xs]) ← 0 ≤ X∧1 > X∧new 4(Xs)
terminization Strategy [8]. This strategy, which we will 24. new 3([X|Xs]) ← 0 > X∧new 1(Xs)
not present here, allows a fully automatic derivation of 25. new 4([X|Xs]) ← 2 ≤ X∧new 6(Xs)
the deterministic, efficient pattern matcher. We unfold 26. new 4([X|Xs]) ← 1 ≤ X∧2 > X∧new 2(Xs)
clause 6 w.r.t. the atom le m([1,0,2], S), that is, we replace 27. new 4([X|Xs]) ← 1 > X∧new 1(Xs)
¯
the atom le m([1,0,2], S) which is an instance of the head 28. new 5([X|Xs]) ←
¯
of clause 1, by the corresponding instance of the body of 29. new 6([X|Xs]) ←
clause 1. We get: This final program is deterministic in the sense that at most
7. le ms (S) ← ap(B, C, S)∧ap(A, Q, B)∧le([1,0,2], Q) one clause can be applied during the evaluation of every
¯ ground goal. As in the case of the Knuth-Morris-Pratt
In order to fold clause 7, we introduce the following defi-
matcher, the efficiency of this final program is very high
nition:
because it behaves like a deterministic finite automaton.
8. new 1(S) ← ap(B, C, S)∧ap(A, Q, B)∧le([1,0,2], Q)
and then we fold clause 7, that is, we replace (the instance 3 Program Synthesis
of) the body of a clause 8 which occurs in the body of
clause 7 by (the corresponding instance of) the head of Program synthesis is a technique for deriving programs
clause 8. We get: from formal, possibly non-executable, specifications (see,
for instance, [11, 24] for the derivation of logic programs
9. le ms (S) ← new 1(S) from first-order logic specifications). In this section we
¯
Then we unfold clause 8 w.r.t. the atoms ap and le and we present an example of use of the program transformation
get: technique for performing program synthesis and deriving
10. new 1([X|Xs]) ← 1 ≤ X ∧ap(Q, C, Xs)∧le([0,2], Q) a constraint logic program from a first-order formula.
11. new 1([X|Xs]) ← ap(B, C, Xs)∧ap(A, Q, B)∧ The example we will present is the N -queens example,
le([1,0,2], Q) which has been often considered in the literature for in-
troducing programming techniques such as recursion and
Then we apply the clause splitting rule to clause 11, by backtracking. The N -queens problem can be described as
separating the cases where 1 ≤ X and 1 > X. We get: follows. We are required to place N (≥ 0) queens on an
12. new 1([X|Xs]) ←1 ≤ X∧ap(B, C, Xs)∧ap(A, Q, B)∧ N×N chess board, so that no two queens attack each other,
le([1,0,2], Q) that is, they do not lie on the same row, column, or diago-
13. new 1([X|Xs]) ←1 > X∧ap(B, C, Xs)∧ap(A, Q, B)∧ nal. By using the fact that no two queens should lie on the
le([1,0,2], Q) same row, we represent the position of the N queens on the
N × N chess board as a permutation L = [i1 , . . . , iN ] of
In order to fold clauses 10 and 12 we introduce the follow-
the list [1, . . . , N ] such that ik is the column of the queen
ing two clauses defining the predicate new 2:
on row k.
14. new 2(Xs) ← ap(Q, C, Xs)∧le([0, 2], Q) A specification of the solution L for the N -queens prob-
15. new 2(Xs) ← ap(B,C,Xs)∧ap(A,Q,B)∧le([1,0,2],Q) lem is given by the following first-order formula ϕ(N, L):
Then we fold clauses 10 and 12 by using the two clauses nat(N ) ∧ nat −list(L) ∧ length(L, N ) ∧
14 and 15 and we also fold clause 13 by using clause 8. ∀X (member (X, L) → in(X, 1, N ))∧
We get the following clauses which define new 1: ∀A,B,K,M
16. new 1([X|Xs]) ← 1 ≤ X∧new 2(Xs) ((1 ≤ K ∧ K ≤ M ∧occurs(A, K, L) ∧occurs(B,M,L))
17. new 1([X|Xs]) ← 1 > X∧new 1(Xs) → (A 6= B ∧ A−B 6= M −K ∧ B −A 6= M −K))
They are mutually exclusive because of the constraints where the various predicates which occur in ϕ(N, L) are
1 ≤ X and 1 > X. Now the program transformation con- defined by the following constraint logic program P :
tinues in a similar way as above: we introduce the new nat(0) ←
predicates new 3 through new 6, we derive their defining nat(N ) ← N = M +1 ∧ M ≥ 0 ∧ nat(M )
clauses, and eventually, we get the following specialized, nat −list([ ]) ←
deterministic program: nat −list([H|T ]) ← nat(H) ∧ nat −list(T )
9
Il Milione: A Journey in the Computational Logic in Italy
length([ ], 0) ← iff M (P ∪ F ) |= queens(N, L) and, thus, Property (π)
length([H|T ], N ) ← N = M +1 ∧ M ≥ 0 ∧ length(T, M ) holds. Moreover, it can be shown that R terminates for all
member (X, [H|T ]) ← X = H queries of the form queens(n, L) and it computes a solu-
member (X, [H|T ]) ← member (X, T ) tion for the N -queens problem in a clever way: each time
in(X, M, N ) ← X = N ∧ M ≤ N a queen is placed on the board, program R tests whether
in(X, M, N ) ← N = K +1 ∧ M ≤ K ∧ in(X, M, K) or not it attacks every other queen already placed on the
occurs(X, I, [H|T ]) ← I = 1 ∧ X = H board.
occurs(X, I +1, [H|T ]) ← I ≥ 1 ∧ occurs(X, I, T )
Now, we would like to synthesize a constraint logic pro- 4 Program Verification
gram R which computes a predicate queens(N, L) such
that the following Property π holds: The proof of program properties is often needed during
(π) M (R) |= queens(N, L) iff M (P ) |= ϕ(N, L) program development for checking the correctness of soft-
ware components w.r.t. their specifications. In this section
where by M (R) and M (P ) we denote the perfect model
we see the use of program transformation for proving pro-
of the program R and P , respectively. By applying the
gram properties specified either by first-order formulas or
technique presented in [9], we start off from the formula
by temporal logic formulas.
queens(N, L) ← ϕ(N, L). From that formula by applying
Proofs performed by using program transformation have
a variant of the Lloyd-Topor transformation [17], we derive
strong relationships with proofs by mathematical induc-
this stratified program F :
tion (see [2] for a survey on inductive proofs). In par-
queens(N, L) ← nat(N ) ∧ nat −list(L) ∧ length(L, N )∧ ticular, the unfolding rule can be used for decomposing
¬aux 1(L, N ) ∧ ¬aux 2(L) a formula of the form ϕ(f (X)), where f (X) is a com-
aux 1(L, N ) ← member (X, L) ∧ ¬in(X, 1, N ) plex term, into a combination of n formulas of the forms
aux 2(L) ← 1 ≤ K ∧ K ≤ M ∧ ϕ1 (X), . . . , ϕn (X), and the folding rule can be used for
¬(A 6= B ∧A−B 6= M−K ∧B−A 6= M−K)∧ applying inductive hypotheses.
occurs(A, K, L) ∧ occurs(B, M, L) It has been shown that the unfold/fold transformations
It can be shown that this variant of the Lloyd-Topor trans- introduced in [3, 26] can be used for proving several kinds
formation preserves the perfect model semantics and, thus, of program properties, such as equivalences of functions
we have that: defined by recursive equation programs [14], equivalences
M (P ∪ F ) |= queens(N, L) iff M (P ) |= ϕ(N, L). of predicates defined by logic programs [20], first-order
properties of predicates defined by constraint logic pro-
The derived program P ∪ F is not very satisfactory from
grams [21], and temporal properties of concurrent sys-
a computational point of view, when using SLDNF reso-
tems [7, 23].
lution with the left-to-right selection rule. Indeed, for a
query of the form queens(n, L), where n is a nonnega-
4.1 The unfold/fold proof method
tive integer and L is a variable, program P ∪ F works by
first generating a value l for L and then testing whether By using a simple example taken from [21], we illustrate
or not length(l, n) ∧ ¬aux 1(l, n) ∧ ¬aux 2(l) holds. This a method based on program transformation, called un-
generate-and-test behavior is very inefficient and it may fold/fold proof method, for proving first-order properties
also lead to nontermination. Thus, the process of pro- of constraint logic programs. Consider the following con-
gram synthesis proceeds by applying the definition, un- straint logic program Member which defines the member-
folding, folding, and goal replacement transformation rules ship relation for lists:
(see [9] for details), with the objective of deriving a more member (X, [Y |L]) ← X = Y
efficient, terminating program. We derive the following member (X, [Y |L]) ← member (X, L)
definite logic program R: Suppose we want to show that every finite list of numbers
queens(N, L) ← new 2(N, L, 0) has an upper bound, i.e., the following formula holds:
new 2(N, [ ], K) ← N = K ϕ : ∀L ∃U ∀X (member (X, L) → X ≤ U )
new 2(N, [H|T ], K) ← N ≥ K +1 ∧ new 2(N, T, K+1)∧ The unfold/fold proof method works in two steps. In the
new 3(H, T, N, 0) first step, ϕ is transformed into a set of clauses by applying
new 3(A, [ ], N, M ) ← in(A, 1, N ) ∧ nat(A) a variant of the Lloyd-Topor transformation [17], thereby
new 3(A, [B|T ], N, M ) ← A 6= B ∧ A−B 6= M +1 ∧ deriving the following program Prop 1 :
B −A 6= M +1 ∧ nat(B) ∧ prop ← ¬p
new 3(A, T, N, M +1) p ← list(L) ∧ ¬q(L)
together with the clauses defining the predicates in and q(L) ← list(L) ∧ ¬r(L, U )
nat. r(L, U ) ← X > U ∧ list(L) ∧ member (X, L)
Since the transformation rules preserve the perfect The predicate prop is equivalent to ϕ in the sense that
model semantics, we have that M (R) |= queens(N, L) M (Member ) |= ϕ iff M (Member ∪ Prop 1 ) |= prop.
10
Il Milione: A Journey in the Computational Logic in Italy
In the second step, we eliminate the existential variables
occurring in Prop 1 (that is, the variables occurring in the ht, A2, B1, B2i
body of a clause and not in its head) by applying the trans- A2 := B2+1
formation strategy presented in [21]. We derive the follow-
ing program Prop 2 which defines the predicate prop: hw, A2, B1, B2i A2 := 0
prop ← ¬p
p ← p1 A2 < B2 ∨ B2 = 0
p1 ← p1
Now, Prop 2 is a propositional program and has a finite per- hu, A2, B1, B2i
fect model, which is {prop}. Since all transformations we
have made can be shown to preserve the perfect model, we Figure 1: The Bakery protocol: a graphical representation
have that M (Member ) |= ϕ iff M (Prop 2 ) |= prop and, of the transition relation tA for the agent A.
therefore, we have completed the proof of ϕ because prop
belongs to M (Prop 2 ). systems (see [5] for a method based on constraint logic
Note that the unfold/fold proof method can be viewed as programming). Due to the above mentioned undecidabil-
an extension to constraint logic programs of the quantifier ity limitation, all these methods are incomplete.
elimination method, which has well-known applications in As an example of use of program transformation for ver-
the field of automated theorem proving (see [22] for a brief ifying CTL properties of infinite state systems, now we
survey). consider the Bakery protocol [15] and we verify that it sat-
isfies the mutual exclusion and starvation freedom proper-
4.2 Infinite-state model checking ties.
Let us consider two agents A and B which want to ac-
Now we present a method for verifying temporal proper-
cess a shared resource in a mutual exclusive way by using
ties of infinite state systems based on the transformation of
the Bakery protocol. The state of agent A is represented by
constraint logic programs [7].
a pair hA1, A2i, where A1 is an element of the set {t, w, u}
As indicated in [4], the behavior of a concurrent system of control states (where t, w, and u stand for think, wait,
that evolves over time according to a given protocol can and use, respectively) and A2 is a counter that takes values
be modeled by means of a state transition system, that is, from the set of natural numbers. Analogously, the state of
(i) a set S of states, (ii) an initial state s0 ∈ S, and (iii) a agent B is represented by a pair hB1, B2i. The state of the
transition relation t ⊆ S × S. We assume that t is a total system consisting of the two agents A and B, whose states
relation, that is, for every state s ∈ S there exists a state are hA1, A2i and hB1, B2i, respectively, is represented by
s0 ∈ S, called successor state of s, such that t(s, s0 ) holds. the 4-tuple hA1, A2, B1, B2i. The transition relation t of
A computation path starting from a (possibly not initial) the two agent system from an old state OldS to a new state
state s1 is an infinite sequence of states s1 s2 . . . such that, NewS , is defined as follows:
for every i ≥ 1, there is a transition from si to si+1 .
The properties of the evolution over time of a concurrent t(OldS , NewS ) ← tA (OldS , NewS )
system are specified by using a temporal logic called Com- t(OldS , NewS ) ← tB (OldS , NewS )
putation Tree Logic (or CTL, for short [4]) which specifies where the transition relation tA for the agent A is given
the properties of the computation paths. The formulas of by the following clauses whose bodies are conjunctions of
CTL are built from a given set of elementary properties of constraints (see also Figure 1):
the states by using: (i) the connectives: ¬ (‘not’) and ∧
tA (ht, A2, B1, B2i, hw , A21, B1, B2i) ← A21 = B2+1
(‘and’), (ii) the following quantifiers along a computation
tA (hw , A2, B1, B2i, hu, A2, B1, B2i) ← A2 < B2
path: g (‘for all states on the path’ or ‘globally’), f (‘there
exists a state on the path’ or ‘in the future’), x (‘next time’), tA (hw , A2, B1, B2i, hu, A2, B1, B2i) ← B2 = 0
and u (‘until’), and (iii) the quantifiers over computation tA (hu, A2, B1, B2i, ht, A21, B1, B2i) ← A21 = 0
paths: a (‘for all paths’) and e (‘there exists a path’). The following analogous clauses define the transition rela-
Very efficient algorithms and tools exist for verifying tion tB for the agent B:
temporal properties of finite state systems, that is, systems tB (hA1, A2, t, B2i, hA1, A2, w , B21i) ← B21 = A2+1
where the set S of states is finite [4]. However, many con-
tB (hA1, A2, w , B2i, hA1, A2, u, B2i) ← B2 < A2
current systems cannot be modeled by finite state systems.
tB (hA1, A2, w , B2i, hA1, A2, u, B2i) ← A2 = 0
Unfortunately, the problem of verifying CTL properties of
tB (hA1, A2, u, B2i, hA1, A2, t, B21i) ← B21 = 0
infinite state systems is undecidable, in general, and thus, it
cannot be approached by traditional model checking tech- Note that the system has an infinite number of states, be-
niques. For this reason various methods based on auto- cause counters may increase in an unbounded way.
mated theorem proving have been proposed for enhancing The temporal properties of a transition system are spec-
model checking and allowing us to deal with infinite state ified by defining a predicate sat(S, P ) which holds if and
11
Il Milione: A Journey in the Computational Logic in Italy
only if the temporal formula P is true at state S. For in- The clauses defining the predicate sat(S, P ) for the case
stance, the clauses defining sat(S, P ) for the cases where where P is a CTL formula of the form af (F ) are:
P is: (i) an elementary formula F , (ii) a formula of the sat(X, af (F )) ← sat(X, F )
form ¬F , (iii) a formula of the form F1 ∧ F2 , (iv) a for- sat(X, af (F )) ← ts(X, Ys) ∧ sat all (Ys, af (F ))
mula of the form ef (F ), are the following ones: sat all ([ ], F ) ←
sat(S, F ) ← elem(S, F ) sat all ([X|Xs], F ) ← sat(X, F ) ∧ sat all (Xs, F )
sat(S, ¬F ) ← ¬sat(S, F ) where ts(X, Ys) holds iff Ys is a list of all successor states
sat(X, F1 ∧ F2 ) ← sat(X, F1 ) ∧ sat(X, F2 ) of X. For instance, one of the clauses defining predicate
sat(S, ef (F )) ← sat(S, F ) ts in our Bakery example is:
sat(S, ef (F )) ← t(S, T ) ∧ sat(T, ef (F )) ts(ht, A2, t, B2i, [hw , A21, t, B2i, ht, A2, w , B21i]) ←
where elem(S, F ) holds iff F is an elementary property A21 = B2+1 ∧ B21 = A2+1
which is true at state S. In particular, for the Bakery pro- which states that the state ht, A2, t, B2i has two possible
tocol we have the following clause: successor states: hw , A21, t, B2i (with A21 = B2+1) and
elem(hu, A2, u, B2i, unsafe) ← ht, A2, w , B21i (with B21 = A2+1).
Let Psf denote the program obtained by adding to Pmex
that is, unsafe holds at a state where both agents A and
the clauses defining: (i) the elementary properties wA and
B are in the control state u (both agents are accessing the
uA , (ii) the atom sat(X, af (F )), (iii) the predicate sat all ,
shared resource at the same time).
and (iv) the predicate ts. In order to verify the starvation
Note that by ef we denote the composition of e (there
freedom property we introduce the clause:
exists a computation path) and f (there exists a state on
the path) and, indeed, sat(S, ef (F )) holds iff there exists (σ) sf ← sat(ht, 0, t, 0i, ¬ef (wA ∧ ¬af (uA )))
a computation path π starting from S and a state s on π and, by applying the definition, unfolding, and folding
such that F is true at s. rules according to the specialization strategy, we transform
The mutual exclusion property holds for the Bakery pro- the program Psf ∪ {σ} into a new program R which con-
tocol if there is no computation path starting from the ini- tains a clause of the form sf ←.
tial state such that at a state on this path the unsafe prop- The derivations needed for verifying the mutual exclu-
erty holds. Thus, the mutual exclusion property holds if sion and the starvation freedom properties were performed
sat(ht, 0, t, 0i, ¬ef (unsafe)) belongs to the perfect model in a fully automatic way by using our experimental con-
M (Pmex ), where: (i) ht, 0, t, 0i is the initial state of the straint logic program transformation system MAP [18].
system and (ii) Pmex is the program consisting of the
clauses for the predicates t, tA , tB , sat, and elem defined 5 Conclusions and Future Directions
above.
In order to show that sat(ht, 0, t, 0i, ¬ef (unsafe)) ∈ We have presented the program transformation method-
M (Pmex ), we introduce a new predicate mex defined by ology and we have demonstrated that it is very effective
the following clause: for: (i) the derivation of correct software modules from
(µ) mex ← sat(ht, 0, t, 0i, ¬ef unsafe) their formal specifications, and (ii) the proof of properties
of programs. Since program transformation preserves cor-
and we transform the program Pmex ∪ {µ} into a new rectness and improves efficiency, it is very useful for con-
program Q which contains a clause of the form mex ←. structing software products which are provably correct and
This transformation is performed by applying the defini- whose time and space performance is very high.
tion, unfolding, and folding rules according to the spe- In order to make program transformation effective in
cialization strategy, that is, a strategy that derives clauses practice we need to increase the level of automation of the
specialized to the computation of predicate mex . From transformation strategies for program improvement, pro-
the correctness of the transformation rules we have that gram synthesis, and program verification. Furthermore,
mex ∈ M (Q) iff mex ∈ M (Pmex ∪ {µ}) and, hence, these strategies should be incorporated into powerful tools
sat(ht, 0, t, 0i, ¬ef (unsafe)) ∈ M (Pmex ), that is, the for program development.
mutual exclusion property holds. An important direction for future research is also the ex-
For the Bakery protocol we may also want to prove the ploration of new areas of application of the transforma-
starvation freedom property which ensures that an agent, tion methodology. In this paper we have described the use
say A, which requests the shared resource, will eventually of program transformation for verifying temporal proper-
get it. This property is expressed by the CTL formula: ties of infinite state concurrent systems. Similar techniques
ag(wA → af (uA )), which is equivalent to: ¬ef ((wA ∧ could also be devised for verifying other kinds of proper-
¬af (uA )). The clauses defining the elementary properties ties and other classes of systems, such as security proper-
wA and uA are: ties of distributed systems, safety properties of hybrid sys-
elem(hw , A2, B1, B2i, wA ) ← tems, and protocol conformance of multiagent systems. A
elem(hu, A2, B1, B2i, uA ) ← more challenging issue is the fully automatic synthesis of
12
Il Milione: A Journey in the Computational Logic in Italy
software systems which are guaranteed to satisfy the prop- [12] J. Jaffar and M. Maher. Constraint logic program-
erties specified by the designer. ming: A survey. Journal of Logic Programming,
19/20:503–581, 1994.
6 Acknowledgements [13] N. D. Jones, C. K. Gomard, and P. Sestoft. Par-
We would like to thank the editors of the Intelligenza tial Evaluation and Automatic Program Generation.
Artificiale Magazine for their invitation to write this pa- Prentice Hall, 1993.
per in honor of Prof. Alberto Martelli. We also thank [14] L. Kott. The McCarthy’s induction principle: ‘oldy’
Prof. Martelli for teaching us the ‘structural way’ of pre- but ‘goody’. Calcolo, 19(1):59–69, 1982.
senting algorithms which we learned from his unification
paper [19]. [15] L. Lamport. A new solution of Dijkstra’s concur-
rent programming problem. Communications ACM,
REFERENCES 17(8):453–455, 1974.
[16] M. Leuschel and M. Bruynooghe. Logic program
[1] A. Bossi, N. Cocco, and S. Etalle. Transforming nor-
specialisation through partial deduction: Control is-
mal programs by replacement. In Proc. Meta ’92,
sues. Theory and Practice of Logic Programming,
LNCS 649, 265–279. Springer-Verlag, 1992.
2(4&5):461–515, 2002.
[2] A. Bundy. The automation of proof by mathematical
[17] J. W. Lloyd. Foundations of Logic Programming.
induction. In A. Robinson and A. Voronkov, editors,
Springer-Verlag, Berlin, 1987. Second Edition.
Handbook of Automated Reasoning, volume I, 845–
911. North Holland, 2001. [18] MAP. The MAP transformation system. http://
www.iasi.cnr.it/ proietti/system.html,
[3] R. M. Burstall and J. Darlington. A transformation
1995–2008.
˜
system for developing recursive programs. J. ACM,
24(1):44–67, January 1977.
[19] A. Martelli and U. Montanari. An efficient unification
[4] E. M. Clarke, O. Grumberg, and D. Peled. Model algorithm. ACM TOPLAS, 4(12):258–282, 1982.
Checking. MIT Press, 2000.
[20] A. Pettorossi and M. Proietti. Synthesis and transfor-
[5] G. Delzanno and A. Podelski. Constraint-based de- mation of logic programs using unfold/fold proofs.
ductive model checking. Int. J. Software Tools for Journal of Logic Programming, 41(2&3):197–230,
Technology Transfer, 3(3):250–270, 2001. 1999.
[6] S. Etalle and M. Gabbrielli. Transformations of CLP [21] A. Pettorossi, M. Proietti, and V. Senni. Proving
modules. Theo. Comp. Sci., 166:101–146, 1996. properties of constraint logic programs by eliminat-
ing existential variables. In Proc. ICLP ’06, LNCS
[7] F. Fioravanti, A. Pettorossi, and M. Proietti. Verifying 4079, 179–195. Springer-Verlag, 2006.
CTL properties of infinite state systems by specializ-
ing constraint logic programs. In Proc. VCL’01, Flo- [22] M. O. Rabin. Decidable theories. In Jon Barwise,
rence (Italy), 85–96. Univ. Southampton, UK, 2001. editor, Handbook of Mathematical Logic, 595–629.
North-Holland, 1977.
[8] F. Fioravanti, A. Pettorossi, and M. Proietti. Special-
ization with clause splitting for deriving determin- [23] A. Roychoudhury, K. Narayan Kumar, C. R. Ramakr-
istic constraint logic programs. In Proc. IEEE Int. ishnan, I. V. Ramakrishnan, and S. A. Smolka. Verifi-
Conf. on Systems, Man and Cybernetics, Hammamet cation of parameterized systems using logic program
(Tunisia), Vol. 1, 188–193. IEEE Computer Society transformations. In Proc. TACAS 2000, Berlin, Ger-
Press, 2002. many, LNCS 1785, 172–187. Springer, 2000.
[9] F. Fioravanti, A. Pettorossi, and M. Proietti. Transfor- [24] T. Sato and H. Tamaki. Transformational logic pro-
mation rules for locally stratified constraint logic pro- gram synthesis. In Proc. Int. Conf. on Fifth Genera-
grams. In Program Development in Computational tion Computer Systems, 195–201. ICOT, 1984.
Logic, LNCS 3049, 292–340. Springer-Verlag, 2004.
[25] H. Seki. Unfold/fold transformation of stratified pro-
[10] J. P. Gallagher. Tutorial on specialisation of logic pro- grams. Theo. Comp. Sci., 86:107–139, 1991.
grams. In Proc. PEPM ’93, Copenhagen, Denmark,
88–98. ACM Press, 1993. [26] H. Tamaki and T. Sato. Unfold/fold transformation
of logic programs. In Proc. ICLP ’84, 127–138, Up-
[11] C. J. Hogger. Derivation of logic programs. Journal psala, Sweden. Uppsala University, 1984.
of the ACM, 28(2):372–392, 1981.
13
Il Milione: A Journey in the Computational Logic in Italy
7 Contacts
Alberto Pettorossi
Dipartimento di Informatica, Sistemi e Produzione, Università di Roma “Tor Vergata”
Via del Politecnico 1,
00133 Roma, Italy
+39 0672597379
pettorossi@disp.uniroma2.it
Maurizio Proietti (Corresponding Author)
Istituto di Analisi dei Sistemi e Informatica, Consiglio Nazionale delle Ricerche
Viale Manzoni 30,
00185 Roma, Italy
+39 067716426
maurizio.proietti@iasi.cnr.it
Valerio Senni
Dipartimento di Informatica, Sistemi e Produzione, Università di Roma “Tor Vergata”
Via del Politecnico 1,
00133 Roma, Italy
+39 0672597717
senni@disp.uniroma2.it
8 Biography
Alberto Pettorossi is professor of Theoretical Computer Science at the Engineering Faculty of the University of Roma
“Tor Vergata”. His research activity has been in the area of rewriting systems and concurrent computation, and it is now
concerned with the automatic derivation, transformation, and verification of programs.
Maurizio Proietti received his Laurea degree in Mathematics from the University of Roma “Sapienza”. He is a senior
researcher at the Istituto di Analisi dei Sistemi e Informatica “A. Ruberti” of the National Research Council (IASI-CNR)
in Roma. His research interests include various aspects of constraint and logic programming, and automatic methods for
the transformation, synthesis, and verification of programs.
Valerio Senni is a Ph. D. student in Information Engineering at the the University of Roma “Tor Vergata”. He holds a
research contract for the development of automatic methods for proving program correctness.
Photograph. A black and white glossy photograph, passport- sized of each author is also required. It will be printed
in the corresponding biography box.
14