Temporal Reasoning and Termination of Programs

ABSTRACT

This paper deals with the relationship between the termination of programs and the vali­ dity of certain modal formulas. We give a complete proof procedure for theses formulas, which will allow to bring the correctness of these programs back to a problem of automated deduction in modal logic.

Many modal logics of programs have been de­ velopped during these last years (PR, HKP, M2]. Particular attention has been paid to their abili­ ty to express many properties of programs [HKP, M2J.

This paper is concerned with the relationship of termination problem for regular programs to the validity of certain formulas in modal logic.

For these formulas we present a proof proce­ dure, very close to the resolution procedure for first-order predicate calculus. We will use this procedure to prove the termination of programs. As in Lucid [Aw] we can consider the set of modal for­ mulas with the proof procedure as a programming language. This way of doing things permits direct reasoning about programs, from their direct manipu­ lation, rather than indirectly via another langua­ ge.

I. Preliminaries

We shall consider as in [M2] the modal sys­ tem S4, for reasoning about programs.

For our formalization of quantificational S4, we start with denumerably infinite lists of indivi­ dual variables x1, x2, x3, ... , n-adic function symbols fn, gn, hn, ... , and n-adic predicate symbols pn, qn, rn, ... .

Atomic formulas as well as negations of ato­ mic formulas are called literals. We adopt the prime symbols & (conjunction),~ (negation) L (ne­ cessity) and (xi) (universal quantification). We use the usual notions of terms and well-formel for­ mulas. Let A, B, C, ..· be arbitrary formulas. For each A, MA is defined as usual as ~L~A. The axioma­ tization of quantificational S4 is obtained by

TEMPORAL REASONING AND TERMINATION OF PROGRAMS

Luis Farinas-del-Cerro

Laboratoire des Langages et Systemes Informatiques Universite Paul Sabatier, Toulouse, France

adding to a habitual formalization of lower predi­ cate calculus (LPC) the following axiom schemes and the following rule of inference

• L(A ~B).~ . LA~ LB
• LA ~ A
• LA ~ LLA
• (x)LA ~ L(x) A
• A /LA

Following the example of Kripke, we define a quantificational S4 modal structure as an ordered triple (G, K, R), where K is a set, R is a relation on K and G is a distinguished element of K, toge­ ther with a function ~ wich assigns to each H a set ~(H), called domain in H. We shall further specify that all domaines are identical. The inter­ pretation f of A at H is defined as in LPC by in­ duction on the number of logical symbols in A. And f(LB,H)=t iff f(B,H')=t for every H'~K such HRH', otherwise f(LB,H)=f.

A sentece A is said to be true in a model U associated with a modal structure (G,K,R) if f(A,G)=t ; it is said to be false in that model if f(A,G)=f . A is said to be valid iff it is true in all its models (for every modal structure), and unsatisfiable iff it is false in all its models.

A set of formulas is said to be consistent if there is no finite subset such that the disjunc­ tion of negations of its elements in a theorem.

II. Programs and modalities

2.1. Assume that a program is represented by a directed graph whose nodes are the labels of this program and whose arcs represent transitions between labels. In the graphs there is only a start node (ls) and a terminal node (lt) [M1J. For an arc (11, 12) the transition has the general form as follows

where x = (x 1 , ... ,xn) is the input variables,

that each note li, one and only one of the condi­ tion, corresponding to the arcs leaving li, is true.

Since modal logic, like classical logic (MI], does not provide a direct tool for speaking about programs, such as the logics of programs [HO, S, PRJ, we must associate to each arc of the graph a modal formula :

where at(li) is a proposition corresponding to the label li· This formula is relative to the forward assignment.

1. If Pis a program and Fp the set of modal formulas associated to the graph of P, then Fp is satisfiable.

This is true since the set of formulas of Fp with the general form M(at(l) & p) is consis­ tent [He].

1. A program P is said to be totally cor­ rect with respect to the specification (p,q) if for every input x 0 , satisfying p(x 0 ), the computa­ tion of P terminates and the final values (z 0 ), upon termination, satisfy q(z 0 ). This property is expressed by the formula (noted by FTC) :

In general, in order to verify this property, we need the following informations :

• the formulas describing the execution of program P,
• the formulas (noted by FE) concerning con­ ditions, assignments and inputs (frame axioms in lM2] ) are as follows

Then we can consider these formulas that express the material properties, (depending on the labels) and formal properties not depending on the labels).

The proof can be obtained by a similar rea­ soning to [MI] ·

III. Deduction

1. I. We will now give a deduction method for the formulas of quantificational S4, whose varia­ bles in the scope of the modal operators are free (noted bv s4+ ).

We consider the formulas Ln the Skolem nor­ mal form

where each (xi) is an universal quantifier (the existential quantifiers have been eliminated by Skolem functions in the usual way [RsJ) and :

- each Ai I S i $ m (clause in the classical terminology [R]) is a disjunction of the form:

- where each Pi I $ i $ k" is a literal, each Fi I $ i $ k' is a conjunction of terms possessing the general form of the clauses, and r·ach Di I ~ i 'k is a disjunction that possesses the gene­ ral form of the clauses.

1. There is an effective proced~re, for constructing, for any given formula of S4+, an equivalent formula in Skolem normal form.
2. Let E = {EI, ... ,En} I.; n < w, be a finite set of expressions. A substitution a is called a unifier of the set E if Eia = Eja for i,j £ {l, ··. ,n}. A unifier a is called the most general unifier if for any unifier a' of E there is a substitution a" such that a'= a. a" [RJ.
3. We consider the set of rules [. i=l, .. L and f . i=l ,2 defined recursively as follows: L I+
4. ]. Elementary rule

1. Extending rules :

[2 [LD ; t-Fj = 6([i [D ; F)) provided fl is L, M or the empty symbol

A{M(D & F)} means that M(D & F)is a subfor­

r 1[A{M(D & F)}]=A{ft10:i[D F])} mula of A.

1. Transforming rule

1. Classical rule

Let A1 and A2 be two cl~uses. We say that A1 and A 2 are resolvable if Ei [A1 ; A 2 1 is defined (i.q. the classical rule is used).

Let Ai be a clause. We say if ri [AJ is defined. that Ai is resolvable

The remaining term obtaine after application of ri and by f i[AJ] (Ei[A1 Az)) from A 1 (A 1 and A2) (or Li) is repres ented

3.5. Let A v A1 and A' v A' 1 be two c lauses with no variables in common. The inference rules :

will be applied if A and A' (or A) are (is) resol­ vables . Where a is the most general unifier used in the classical rule.

1. Let A v A 1 v A2 be a c lause.

The inference rule

will be applied if A 1 and A 2 have most general unifier a.

3.4. Let S be a finite set of clauses, a de­ duction of A from S is a finite sequence of clau­ ses A 1 , ... ,An, such that :

• -~is A

- Ai I ~ i < n is

• an element of S, or
• a factor (rule 3) of Aj, j < i, or
• a r esolvent (rules 1 or j,k < i and 2) of Aj and Ak

3.5. A set S of clauses is unsatisfiable iff there is a deduction of the empty clause from S.

The proof can be obtained as in [F) or [o).

IV. Example

Consider the program P (fig. I) over the in­ tegers, that adds an integer x 1 to a natural number x 2 - The clauses as set out in 3. corresponding to this program are of the form

Using the induction formula :

And the frame clauses

1. M(x -f O)v L (x 0)
2. L("" 0 f 0)

The program considered will be totally cor­ rect if this set of clauses with the following formula :

Using the method given in 3. we obtain many steps, but here we will give the alternate steps as follows :

1. MM(at(lt) & p(x 1 ,x 2 ,y 1 ,0) & L(~at(lt) v p(x 1 ,x 2 ,y 1 ,0) )) v M((1Bt(l 1 ) v ~ ( x 1 , x 2 ,y 1 ,y 2 )) & a t(l 1 ) & y 2 >0 & p(x 1 ,x 2 , x 1 +1, y 2 -l))v L (~at(l 1 ) v ~p(x 1 ,x 2 ,y 1 ,y 2 ) v M(a t(lt) & p( x1,x2,y1,0))

from 4. ,3. ,5<~nd 6.

1. M5(~at(l 1 ) v ~(x 1 ,x 2 ,y 1 ,y 2 )) & at(l 1 ) & y 2 >0 & p(x 1 ,x 2 ,x 1 +1,y 2 -1)) v L (~at(l 1 ) v ~(x 1 , x 2 ,y 1 ,y 2 ) v M(at(lt) & p(x 1 , x 2 ,y 1 ,0)) from8.
2. MM(~at(l 1 ) v y 2 >o v ~(x 1 ,x 2 ,y 1 +1,y 2 -1) & a t(l 1 ) & y 2 >0 & p(x 1 ,x 2 ,x 1 +1, y 2 -1)) v L (~at(l 1 ) v ~( x 1 ,x 2 ,y 1 , y 2 ) v M(at(lt) & p(x1,x2,y1,0))

fr om 9. and 2.

1. from 10., 7. and I.

And from 11. and at(ls) & p(x 1 ,x 2 ,y 1 ,y 2 ) we obtain the empty clause.

This proof is very close to the Lucid (AW~ version of intermittent assertion proofs LMW].

The different rules (concatenation, consequen­ ce ... ) can be obtained by putting together several steps of our method.

In general, we can consider the set of modal formulas with the proof procedure as a programming language, that permits direct reasoning about the programs, from their direct manipulation.

BIBLIOGRAPHY

• Ascroft, E., Wadge, W. "Intermittent asser­ tion proofs in Lucid". in IFIP 77, pp. 723726 .
• fariii.as -del-Cerro, L. "A deduction method for modal logic". European AI Conference, 11-14 July 1982, Orsay.
• ~KP] Harel, Kazen, Parikh, "Process logic, expres­ siveness, decidability, completeness". in FOGS 80, pp. 129-142.
• ~o] Hoare, "An axiomatic basic of computer pro­ gramming". in Com. ACM, 12, 10, (1969).
• [!ic) Hugues, Cressyell, "An introduction to modal logic", Mathuem & Co., London, (1978).
• Manna, Z. "Properties of programs and first order predicate ca lculus", in J.A.C.M., 16, 2, (1969), pp. 244-255.
• Manna, z. "Logics of Programs", in Proc. IFIP 80, North-Holland, pp. 41-52.
• Manna, Z., Waldinger, R. "Is "sometime" sometime better than "always" ? : Intermit­ tent assertions in proving program correct­ ness", in Com. ACM, 21, 2, (1978), pp. 159172.
• Orlowska, E. "Resolution systems and their applications", I, II, Fundamenta Informati­ ~· (1980), pp. 235-267, 333- 362.
• Pratt, V. R. "Semanti cal Considerations on Floys-Hoare Logic", in Proc. 17th Ann. IEEE Symp. on Foundations of Comp . Sci., (1976); pp. 109-121.
• Rasiowa, Sikorski, "The mathematics of ma­ thematics", Warszowa, ( 1963).
• Robinson, "A machine oriented logic based on the r esolution principle", in J .A. C.M., 12, ( 1965) · pp. 23-41 .
• Salwicki, "Fromatized a lgorithme language", in Bul. Ac. Pol. Sci., 18, 5, (1970), pp. 227-232.