The subject of this paper is a program veri cation method that takes into account abortion caused by partial functions in program statements. In particular, boolean expressions of various statements will be investigated that are not well-de ned. For example, a loop aborts if its execution begins in a state for which the loop condition is undened. This work considers the program constructs of nondeterministic sequential programs and also deals with the synchronization statement of parallel programs introduced by Owicki and Gries [Owi76]. The syntax of program constructs will be reviewed and their semantics will be formally de ned in such a way that they suit the relational model of programming developed at Eotvos Lorand University [Fot88, Fot95]. This relational model de nes the program as a set of its possible executions and also provides de nition for other important programming notions, like problem and solution. The proof rules of total correctness [Dij76, Fot05, Gri81, Hoa69, Owi76] will be extended by treating abortion caused by partial functions. The use of these rules will be demonstrated by means of a veri cation case study.
There are programs that have to work without any error. To be able to reason about the correctness of such programs we need to have rigorous de nition of the semantics of the language of these programs. We also need methods that allow us to verify the correctness of programs. When one provides the semantics of a program construct, the functions that are used to build the programming statement (loop condition for example) are assumed to be total functions. The veri cation methods also consider program descriptions where these functions are well-de ned.
This paper focuses on partial functions in program descriptions. In particular, not well de ned boolean expressions of various statements will be considered. They will be taken into account when providing the semantics of statements. The semantics of program constructs are given in such a way that they suit an existing relational programming model. This model de nes the basic concepts of programming, for example de nes the program as a set of its possible executions. A veri cation method will be presented as well, that handles statements containing partial logical functions. Some rules of the veri cation method are well known, the new rules will be given along with their proof.
The rest of this paper is organized as follows. Section 2 reviews how partial functions are handled in the literature. Section 3 introduces keywords that are allowed to use to build programs we want to investigate. Next, the semantics of these elementary programs and construct are provided. The mentioned relational programming model is also presented here shortly. Then we provide veri cation rule for each statement that can be formed from our keywords. Section 4 presents a veri cation example and illustrates the use of the veri cation rules given in the previous section. Section 5 summarizes our approach and work. 2
Z. Manna in [Man74] presents a veri cation method for owchart programs. A owchart program is a diagram constructed by edges and nodes, where the nodes denote statements. y g(x; y) stands for an assignment statement where g(x; y) is a total function mapping Dx Dy into Dy.
C. A. Hoare in [Hoa69] did not mention that the conditions of the alternative or loop constructions were total logical functions but his examples showed this.
K. R. Apt and E.-R. Oderog use total logical functions namely Boolean expressions in their work. For example, to ensure that the expressions x div y and x mod y are total they additionally stipulate x div y = 0 and x mod y = x for the special case of y = 0 [Apt97].
D. Gries in his fundamental work on investigating program correctness states that the guards 1, . . . n have to be well-de ned boolean expressions to make sure that the alternative command avoids abortion. However, in his veri cation rules, by assuming that all boolean expressions used in program descriptions (i.e. loop conditions, guards of guarded commands) are well-de ned, he eliminates this condition to make the veri cation rules simpler [Gri81].
Williem-Paul de Roever et al. extend Floyd's inductive assertion method for proving sequential transition systems. In sequential transition systems edges are labelled by commands in the form of c ! f . In their work c has to be a total boolean condition, but partial state transformations that might lead to runtime error (for example c ! x := 1=y where c is the guard of the command x := 1=y) are allowed to use. They present a method for proving that the execution of a given program will not apply unde ned operations [Roe01]. 3 3.1
A parallel nondeterministic program (let S denote it) can be described with a nite string of symbols including the keywords skip, abort, if, , while, do, od, [, ], await, then, ta, parbegin, k and parend, which is generated by the following grammar:
S1; S2 j if 1 ! S1 S =skip j abort j v := f (v) j [S0] j await : : : (resulting fail), the v := f (v) is the nondeterministic assignment, the (S1; S2) is the sequential compisition, the if 1 ! S1 : : : n ! Sn is the nondeterministic conditional statement, the while do S0 od is the loop, the [S0] is the atomic region, the await then S0 ta is the await-statement, and parbegin S1 k k Sn parend is the parallel composition. 3.2
Before the semantics of the elementary programs and the program constructions described above are shown the concept of the program must be clari ed.
All concepts of our programming model as like as the concept of the program are based on the state space. The concept of the state space has already been interpreted in several ways. For many people, the state space is a model of a von Neumann type of computer, others, e.g. Dijkstra [Dij76], associate this notion with the problem to be solved where a state is a compound of the values of the main data types. So, the program is \outside" of the state space operating on it. In our programming model, this second meaning is used. In [Fot88], the notion of the state space is a Cartesian product of the type value set of data types. The only mistake of this obvious de nition is that it imposes an order on the components. In [Fot05, Gre12], this mistake has been repaired.
A program is the complex of its executions. An execution is a sequence of states. A program, by de nition, can always begin, i.e. at least one execution has to start from each state. The program is nondeterministic because several executions may start from the same state and nobody knows which execution will happen. The rst state (start state) of all executions and the last, if the execution is nite, are in the so called base state space. Namely the state space can be permanently changed; the inner states of the executions may have got new components because the program can create and destroy new components (variables) during its execution, so the state space changes dynamically. Two constraints are given: all new components have to be destroyed at the termination, at the very latest, but the base variables should never be removed. The current state always contains the components of the base state space. The variables of the base state space are the base variables; the other variables are the auxiliary variables of the program. Thus the base state space is always a subspace of the current state space. The case when the execution of a program goes wrong will be denoted by a nite sequence of states where the last state is the fail.
A sequence can be given by the enumeration of its elements between the signs "<" and ">": < e1; e2; >. We will use the interconnection of two sequences if the end of the rst sequence is identical to the front of the second one. More precisely, if =< a1; : : : ; an > and =< b1; b2; > are sequences and an = b1 6= fail, then their interconnection is =< a1; : : : ; an; b2; >.
The formal de nition of the program [Gre12] requires some notions. Let H denote the set of all nite and in nite sequences of the elements of set H. H1 includes the in nite sequences; H contains the nite ones. So, H = H [ H1 and H \ H1 = ;. The length of the sequence 2 H is j j, the value of which is 1 if the sequence is in nite.
De nition 1. Let A be the so-called base state space and A be the set of all states which belong to the state spaces B whose subspace is A, i.e. A = S B. A does not contain the state fail. The relation S A (A [ ffailg)
A B is a program over A, if 2. 8a 2 A and 8 2 S(a) : j j 1 and
1 = ai 3. 8 4. 8 2 RS and 8i(1
i < j j) : i 6= fail 2 RS : j j < 1 !
j j 2 A [ ffailg
Now, we are going to give the semantics of the elementary programs and program constructions so that they are treated as programs in the sense of the previous de nition. Our aim is to de ne the set of state-sequences that are mapped to an arbitrary state by a construction.
De nition 2. Let A be a state space and
2 A be the current state. skip( ) ::= f< >g (v := f (v))( ) ::= (S1; S2)( ) ::= f j (if 1 ! S1
: : : where !( ) =
f< ; fail >g (f< ; 0 >j 0 2 f ( )g if if abort( ) ::= f< ; fail >g
A
De nition 7. Let A be the common base state space of the program S0 and the condition . Let current state. 2 A be the De nition 9. Let A be the common base state space of the program S0 and the condition . Let current state. 2 A be the (await
8>[S0]( ) then S0 ta)( ) ::= <(skip; await >:f< ; fail >g
if then S0 ta)( ) if if 2 D ^ ( ) 2 D ^ : ( ) 2= D
Before the de nition of the parallel composition the concept of the \uninterrupted" must be intoduced. Let S be a program and be an arbitrary state of its base state space. The execution S( ) is uninterrupted if the program S is the skip, abort, an assignment statement, an atomic region [P ] or an await statement await then S0 ta where 2= D or ( ) is true. (In these cases the await statement is the abort or the atomic region [S0].)
We must remark that in case of S( ) is not uninterrupted (where is an arbitrary state and S is a program), then S can be always splitted into two programs so that S( ) = (u; T )( ) so that u( ) is uninterrupted. This u is named as the rst statement of S and T is the remainder part of S relative to the state .
If S = await then S0 ta and 2 D ^ : ( ), then u is skip and T is await then S0 ta.
If S = (S1; S2) and S1( ) is uninterrupted, then the u is S1 and T is S2.
If S = (S1; S2) and S1( ) is not uninterrupted, then u is the rst statement of S1 and T is the sequence (T1; S2) where T1 is the remainder part of S1.
If S = while (parbegin S1 k
k Si k where Bi( ) = 3.3
If S = if 1 ! S1 : : : n ! Sn (9i 2 [1::n] : 2= D i _ 8i 2 [1::n] : and one of its conditions is not de ned or all conditions are false in 2 D i ^ : i( )), then u is abort and T is abort. 1 ! S1 : : : n ! Sn and all conditions are de ned and some of them are true in 2 D i ^ 9i 2 [1::n] : i( )), then u is skip and T is Si assuming the ith branch is selected by do S0 od and its condition is not de ned ( 2= D ), then u is abort and T is abort.
If S = while do S0 od and the condition is false in part of S is skip.
If S = while do S0 od and the condition is true in (S0; while do S0 od). ( 2 D ^ : ( )), then u is skip and the reminder ( ^ ( )), then u is skip and T is If S = parbegin P1 k k Pi k k Pn parend and its ith branch is selected by the scheduler and Pi( ) is uninterrupted, then u is Pi and T is parbegin P1 k k Pi 1 k Pi+1 k k Pn parend. If S = parbegin P1 k k Pi k k Pn parend and its ith branch is selected by the scheduler and Pi( ) is not uninterrupted, then u is the rst statement of Pi and T is parbegin P1 k k Ti k k Pn parend where Ti is the remainder part of Pi.
De nition 10. Let A be the common base state space of the programs S1; : : : ; Sn and 2 A be the current state.
n k Sn parend)( ) ::= S Bi( )
i=1 8>(Si; parbegin S1 k k Si 1 k Si+1 k >>< if Si( ) is uninterrupted
k Sn parend)( ) >>(ui; parbegin S1 k k Si 1 k Ti k Si+1 k k Sn parend)( ) :> if Si( ) = (ui; Ti)( ) where ui( ) is uninterrupted Informally, a program is correct if it satis es the intended input/output relation. Program correctness is expressed by so-called correctness formulas. These are statements of the form
ffQggSffRgg where S is a program and Q and R are assertions. The assertion Q is the precondition of the correctness formula and R is the postcondition. The precondition describes the set of initial states in which the program S is started and the postcondition describes the set of desirable nal states.
More precisely: a correctness formula is true if every excecution of S that starts in a state satisfying Q is nite (it terminates) and its nal state satis es R. (This is the concept of the total correctness. The partial correctness is omitted in this paper.)
Reasoning about correctness formulas in terms of semantics is not very convenient. Hoare has introduced a proof system allowing us to prove partial correctness of deterministic programs in a syntax-directed manner, by induction on the program syntax [Hoa69]. Dijkstra, Gries and Owicki have developed this system for nondeterministic and parallel programs [Dij76, Gri81, Owi76]. Now this system is going to be extended.
The rst six rules are well-known, they are only shown for the sake of completeness without their proofs.
Q =) R ffQgg skip ffRgg Q =)
v 2 Df ^ 8e 2 f (v) : Rv e ffQgg v := f (v) ffRgg
The Rv e means that the components of v must be substituted for the corresponding components of e. In that case when the relation f A A of the assingment is a total function, i.e., f is a (deterministic) function mapping from A to A and Df = A, the rule of assigment can be written in the following form. Theorem 3. Let Q and R be two assertions, S be a program.
Theorem 4. Let Q and R be two assertions, S1 and S2 be two programs.
Q =) Rv f(v) ffQgg v := f (v) ffRgg ffQgg S ffRgg ffQgg [S] ffRgg
9Q0 : A ! L ffQgg S1 ffQ0gg ffQ0gg S2 ffRgg ffQgg (S1; S2) ffRgg ffQgg S ffRgg ffQgg S ffRgg Theorem 5. Let Q and R be two assertions, and S stand for the program S annotated with assertions such as preconditions of the assignments or invariants of the loops.
The next three rules take into consideration the cases when some logical functions of the construction is not well-de ned. These rules are the extensions of the well-known versions that use well-de ned logical functions. An assertion P will be interpreted as the set of states that satisfy P many times in the following rules. From its context it can be decided which interpretation holds. For example, Q and R are assertions in the expression Q =) R but they are sets in Q R.
Theorem 6. Let Q and R be two assertions, and S1; : : : Sn be programs and 1; : : : n be conditions.
Q =) Q 1 _
_ n D 1 \
\ D n ffQgg if 1 ! S1 8i 2 f1; : : : ; ng : ffQ ^ igg Si ffRgg : : : ffRgg Proof. We must show that the executions of the conditional statement starting from Q nish at R. Let q be an arbitrary state of Q. Since Q D 1 \ \ D n and Q =) 1 _ _ n, according to the de nition each execution of the conditional statement starting from q belongs to the executions of the component Si where its condition i is satis ed by q.
These executions terminate in a state satisfying R because 8i 2 f1; : : : ; ng : ffQ ^ iggSiffRgg thus ffQgg if 1 ! S1 : : : n ! Sn ffRgg holds.
Theorem 7. Let Q and R be two assertions, and S0 be a program and I ^ : I ^
D =) R =) t
0 ffI ^ gg S0 ffIgg 8c0 2 Z : ffI ^ ffQgg while ^ t = c0gg S0 fft < c0gg do S0 od ffRgg Proof. We need to prove that the executions of the loop starting from Q are nite and they nish at R. Let q be an arbitrary state of Q. Since Q =) I and I D thus q 2 D .
The execution starting from q can be splitted into the sections of the executions generated by the body S0. Each section is started at a state satisfying I ^ and terminates at a state satisfying I (see the cond. ffI ^ ggS0ffIgg). If the total execution is nite, its last section nishes at a state satisfying : or the state q own satis es : if the loop stops at once. It means that each nite execution strating from q nishes at a state of R since I ^ : =) R.
The proof will be complete if we show that there is no in nite execution from q. If there would be an in nite execution, it should consist of in nite sections. Let us consider the in nite sequence of integers that is mapped from the beginning states of the sections by the function t. Because of the criterion 8c0 2 Z : ffI ^ ^ t = c0gg S0 fft < c0gg this sequence should be strictly monotone decreasing thus it should contain negative numbers. However all numbers must be nonnegative because of the criterion I ^ =) t 0. This is a contradiction. Theorem 8. Let Q and R be two assertions, and S0 be a program and Proof. It is enough to show that the executions of the conditional statement starting from Q nish at R. Let q be an arbitrary state of Q. If q 2 D and q satis es , the executions of the await-statement starting from q are identical to the executions of the atomic region S0 starting from q. These executions nish at a state in R because of ffQ ^ gg S0 ffRgg.
The last rule is about the parallel composition.
Theorem 9. Let Q; Q1; : : : Qn and R; R1; : : : Rn be assertions, S1; : : : Sn be programs, and S1 ; : : : Sn be the annotations of the corresponded programs.
Q =)
Q1 ^ : : : ^ Qn 8i 2 f1; : : : ; ng : ffQiggSi ffRigg and they are interference free
R1 ^ : : : ^ Rn ffQgg parbegin S1 k
=) R k Sn parend ffRgg where standard proof outlines ffQiggSi ffRigg, i 2 f1; : : : ; ng, are called interference free if no normal assignment or atomic region u of a component program Si interferes with the proof outline ffQj ggSj ffRj gg of another component program Sj where i 6= j. We say that u does not interfere with ffQggS ffRgg if the following conditions are satis ed: 1. for all assertions r in ffQggS ffRgg the formula ffr ^ pre(u)gguffrgg holds, where pre(u) is the precondition of u in the annotation S , 2. for all termination function t : A ! Z in ffQggS ffRgg where A is the base state space of the parallel composition the formula ffpre(u) ^ t = c0gg u fft c0gg holds, where c0 is an arbitrary integer. 4
Consider the following problem: given an array x of n integer numbers and an integer number k. Count the elements of x that are divisors of k.
Speci cation of the problem can be given in the following way: A = (x : Zn; k : Z; count : N) P re = (x = x0)
n P ost = (P re ^ count = P (x[j] j k))
j=1 where : L ! f0; 1g and (true) = 1 and (f alse) = 0
Let S denote the following program: i; count := 1; 0 while i n do
if od x[i] j k ! count := count + 1 x[i] - k ! skip Let Q0 denote the intermediate assertion of the sequence S, between the initialisation and the loop, Q00 the intermediate assertion that holds before executing the assignment i := i + 1, Inv the invariant and t the variant function of the loop.
Now we shall to prove that ffP regg S ffP ostgg holds. Since S is a sequence, due to Theorem 4. it is su cient to prove that 1. ffP regg i; count := 1; 0 ffQ0gg and 2. ffQ0gg DO ffP ostgg, where DO denotes the loop: while i n do if x[i] j k ! count := count + 1 and Q0 = (P re ^ count = 0 ^ i = 1) is given.
Let us prove the two conditions:
x[i] - k ! skip ; i:=i+1 od 1. ffP regg i; count := 1; 0 ffQ0gg
By replacing i with 1 and count with 0 in Q0 we obtain (P re ^ 0 = 0 ^ 1 = 1), that is P re. Obviously P re =) P re holds. We proved that P re =) Q0i 1;count 0 holds. Now, by the remark of Theorem 2. ffP regg i; count := 1; 0 ffQ0gg is deduced. 2. ffQ0gg DO ffP ostgg
Instead of proving this veri cation condition, due to Theorem 7. it is su cient to prove that (a) Q0 =) Inv and (b) Inv
Di n and (c) Inv ^ :(i (d) Inv ^ i n =) n n) =) P ost and
i 0 and (e) 8c0 2 Z : ffInv ^ i n ^ n i = c0gg S0 ffInv ^ n (b) Inv Di n
Since i n is a well-de ned logical function, its domain contains all states of the statespace, including those that satisfy Inv. (c) Inv ^ :(i
n) =) P ost i. P re
The invariant contains the precondition, therefore Inv implies P re.
n ii. count = P (x[j] j k)
j=1 Since i 2 [1::n + 1] and :(i
n), therefore we get i = n + 1.
i 1 This, together with count = P j=1
(j j k)) we know from Inv, yields the desired condition. (d) Inv ^ i n =) n i 0
This holds because due to the loop condition i
n is true. (e) 8c0 2 Z : ffInv ^ i n ^ n i = c0gg S0 ffInv ^ n i < c0gg
Let c0 be an arbitrary integer number. Since the loop body S0 is a sequence, we use Theorem 4. with Inv ^ i n ^ n i = c0 as Q and with Inv ^ n i < c0 as R. It is su cient to prove the following two conditions: i. ffInv ^ i n ^ n ii. ffQ00gg i := i + 1 ffP ^ n i = c0gg IF ffQ00gg and where IF denotes the conditional statement if x[i] j k ! count := count + 1 x[i] - k ! skip and the intermediate assertion of the loop body is Q00 is given: Q00 = Invi i+1 ^ n i = c0 i. ffInv ^ i n ^ n i = c0gg IF ffQ00gg
Due to Theorem 6., the following conditions are su cient to prove: A. Inv ^ i n ^ n i = c0 =) (x[i] j k _ x[i] - k) and B. Inv ^ i n ^ n i = c0 Dx[i]jk \ Dx[i]-k and C. ffInv ^ i n ^ n i = c0 ^ x[i] j k ^ n i = c0gg count := count + 1 ffQ00gg and D. ffInv ^ i n ^ n i = c0 ^ x[i] - k ^ n i = c0gg skip ffQ00gg Let us prove the conditions separately: A. Inv ^ i n ^ n i = c0 =) (x[i] j k _ x[i] - k)
For each state of the statespace for which Inv ^ i n ^ n i = c0 holds, either x[i] is a divisor of k or x[i] is not a divisor of k.
B. Inv ^ i n ^ n i = c0 Dx[i]jk \ Dx[i]-k
In order to ensure that x[i] j k and x[i] - k are well-de ned functions, we have to take into account not only that the divisibility x[i] j k can be answered only if x[i] is not zero, but the index i has to be inside the bounds of the array x. More precisely, we want to prove that Inv ^ i n ^ n i = c0 =) i 2 [1::n] ^ x[i] 6= 0 ^ i 2 [1::n] ^ x[i] 6= 0.
Although i 2 [1::n + 1] (due to the invariant) and the loop condition i n together allow us to deduce that i 2 [1::n] holds, we cannot guarantee that each state of the statespace for which Inv ^ i n ^ n i = c0 holds, x[i] is not 0. The reason is, that there is no assumption for the elements of x, except that they are integer numbers. The case when x[i] = 0, is not excluded by any condition we know and are allowed to use. If x[i] equals 0, the expressions x[i] j k and x[i] - k have no de ned value. The current condition cannot be proven. We provide the remaining part of the proof for the sake of completeness. i 1 Q00count count+1 = (P re ^ i + 1 2 [1::n + 1] ^ count + 1 = P j=1 C. ffInv ^ i n ^ n i = c0 ^ x[i] j k ^ n
Let us recall that Q00 is (Invi i+1 ^ n i = c0gg count := count + 1 ffQ00gg i = c0).
(x[j] j k)) + (x[i] j k)). By Theorem 2. it is su cient to prove that (Inv ^ i n ^ n i = c0 ^ x[i] j k ^ n
i = c0) =) Q00count count+1. P re P re in included in Inv. i + 1 2 [1::n + 1] Due to the invariant i 2 [1::n + 1] holds. This, combined with the loop condition i i + 1 2 [1::n + 1]. i = 1 and i n.
i 1 count + 1 = P (x[j] j k)) + (x[i] j k)) j=1
i 1 By the loop invariant Inv, count = P
j=1 (x[i] j k) = 1, we added 1 to both sides of the previous equation.
(x[j] j k)). Since in this case x[i] is a divisor of k, n implies D. ffInv ^ i n ^ n i = c0 ^ x[i] - k ^ n
Let us recall that Q00 is (Invi i+1 ^ n i 1 P (x[j] j k)) + (x[i] j k) ^ n j=1 (Inv ^ i n ^ n i = c0 ^ x[i] - k ^ n i = c0) =) Q00.
P re P re in included in Inv. i + 1 2 [1::n + 1] We prove this in the same way as we did in the previous case.
i 1 count = P (x[j] j k)) + (x[i] j k)) j=1 i = c0gg skip ffQ00gg i = c0) that is (P re ^ i + 1 2 [1::n + 1] ^ count = i = c0). By Theorem 1. it is su cient to prove that
i 1 By the loop invariant Inv, count = P (x[j] j k)). Since in this case x[j] is not a divisor of k, j=1 (x[i] j k) evaluates to zero. The desired condition holds because both sides of the equation i 1 count = P (x[j] j k)) in Inv remained the same.
j=1 n i = c0
It is obviously true, since it is on the left side. ii. ffQ00gg i := i + 1 ffInv ^ n i < c0gg
Q00 = (Invi i+1 ^n i = c0. It is obvious that (Invi i+1 ^n i = c0) =) (Inv ^n i < c0)i i+1, therefore by Theorem 2 we get the expected correctness formula.
To prove the correctness formula ffQgg S ffRgg, all the veri cation conditions generated by the veri cation rules have to be satis ed. Let us remember that the following condition was not proven: Inv ^ i n ^ n i = c0 Dx[i]jk \ Dx[i]-k We could not guarantee that both of the logical functions x[i] j k and x[i] - k are well-de ned functions. Evaluating these functions of the program might lead to abortion. The rest of the conditions were unnecessary to prove, their proof was given for the sake of completeness. 5
The main idea behind this work is to take into account abortion caused by partial functions in programs and extend veri cation rules to be able to ensure that such programs are total correct. To reason about correctness, we provided the formal de nition of the semantics of programs under our investigation. One of the contributions of this paper is, that the semantics of program constructs are de ned in such a way that they suit an existing relational model of programming. This relational model de nes the program as a set of its possible executions and also provides de nition for other important programming notions like problem and solution. Then, for each class of statements we provide a veri cation rule. The rst six rules are well-known. Three rules are new, they are presented along with their proofs. The use of the rules is demonstrated by means of a veri cation case study. [Apt97] K. R. Apt, E.-R. Olderog. Veri cation of Sequential and Concurrent Program. Springer-Verlag, 1997.
W.-P. de Roever et al. Concurrency Veri cation. Cambridge University Press, 2001.