Special Issue on ICIT 2009 Conference - Bioinformatics and Image

TESTING OF PROGRAM CORRECTNES

IN FORMAL THEORY

Ivana Berkovic
University of Novi Sad, Technical Faculty Mihajlo Pupin, Zrenjanin, Serbia
[email protected]

Branko Markoski
University of Novi Sad, Technical Faculty Mihajlo Pupin, Zrenjanin, Serbia
[email protected]

Jovan Setrajcic
University of Novi Sad, Faculty of Sciences, Novi Sad, Serbia
[email protected]

Vladimir Brtka
University of Novi Sad, Technical Faculty Mihajlo Pupin, Zrenjanin, Serbia
[email protected]

Dalibor Dobrilovic
University of Novi Sad, Technical Faculty Mihajlo Pupin, Zrenjanin, Serbia
[email protected]

ABSTRACT
Within softwares life cycle, program testing is very important, since quality of
specification demand, design and application must be proven. All definitions related
to program testing are based on the same tendency and that is to give answer to the
question: does the program behave in the requested way? One of oldest and best-
known methods used in constructive testing of smaller programs is the symbolic
program execution. One of ways to prove whether given program is written correctly
is to execute it symbolically. Ramified program may be translated into declarative
shape, i.e. into a clause sequence, and this translation may be automated. Method
comprises of transformation part and resolution part.This work gives the description
of the general frame for the investigation of the problem regarding program
correctness, using the method of resolution invalidation.. It is shown how the rules
of program logic can be used in the automatic resolution procedure. The examples of
the realization on the LP prolog language are given (without limitation to Horn's
clauses and without final failure).. The process of Pascal program execution in the
LP system demonstrator is shown.

Keywords: program correctness, resolution, test information, testing programs

1. INTRODUCTION testers (persons performing tests) in case when test

finds no errors. Conflict between these two goals in
The program testing is defined as a process of visible when a testing process finds no error. In
program execution and comparison of observed absence of other information, this may mean that
behaviour to behaviour requested. The primary goal the software is either of very high or very poor
of testing is to find software flaws [1], and quality.
secondary goal is to improve self-confidence in Program testing is, in principle, complicated

UbiCC Journal Volume 4 No. 3 618

Special Issue on ICIT 2009 Conference - Bioinformatics and Image

process that must be executed as systematically as According to [5] testing may be descriptive and
possible in order to provide adequate reliability and prescriptive. In descriptive testing, testing of all test
quality certificate. items is not necessary. Instead, in testing log is
Within software lifespan, program testing is one written whether software is hard to test, is it stable
of most important activities since fulfillment of or not, number of bugs, etc... Prescriptive testing
specification requirements, design and application establishes operative steps helping software control,
must be checked out. According to Mantos [2], big i.e. dividing complex modules in several more
software producers spend about 40% of time for simple ones. There are several tests of complex
program testing. In order to test large and software measurements. Important criterion in
complicated programs, testing must be as measurement selection is equality (harmony) of
systematic as possible. Therefore, from all testing applications. It is popular in commercial software
methods, only one that must not be applied is ad application because it guarantees to user a certain
hoc testing method, since it cannot verify quality level of testing, or possibility of so-called internal
and correctness regarding the specification, action [6]. There is a strong connection between
construction or application. Testing firstly certifies complexity and testing, and methodology of
whether the program performs the job it was structural testing makes this connection explicit [6].
intended to do, and then how it behaves in different Firstly, complexity is the basic source of software
exploitation conditions. Therefore, the key element errors. This is possible in both abstract and concrete
in program testing is its specification, since, by sense. In abstract sense, complexity above certain
definition, testing must be based on it. Testing point exceeds ability of the human mind to do an
strategy includes a set of activities organized in exact mathematical manipulation. Structural
well-planned sequence of steps, which finally programming techniques may push these barriers,
confirms (or refutes) fulfillment of required but may not remove them completely. Other
software quality. Errors are made in all stages of factors, listed in [7], claim that when module is
software development and have a tendency to more complex, it is more probable that it contains
expand. A number of errors revealed may rise an error. In addition, above certain complexity
during designing and then increase several times threshold, probability of the error in the module is
during the coding. According to [3], program- progressively rising. On the basis of this
testing stages cost three to five times more than any information, many software purchasers define a
other stages in a software life span. number of cycles (software module cyclicity,
In large systems, many errors are found at the McCabe [8] 1) in order increase total reliability. On
beginning of testing process, with visible decline in the other hand, complexity may be used directly to
error percent during mending the errors in the distribute testing attempts in input data by
software itself. There are several different connecting complexity and number of errors, in
approaches to program testing. One of our order to aim testing to finding most probable errors
approaches is given in [4]. Testing result may not ("lever" mechanism, [9]). In structural testing
be predicted in advance. On the basis of testing methodology, this distribution means to precisely
results it may be concluded how much more errors determine number of testing paths needed for every
are present in the software. software module being tested, which exactly is the
The usual approach to testing is based on cyclic complexity. Other usual criteria of "white
requests analyse. Specification is being converted box" testing has important flaw that may be
into test items. Apart of the fact that incorrigible fulfilled with small number of tests for arbitrary
errors may occur in programs, specification complexity (using any possible meaning of the
requests are written in much higher level than "complexity") [10].
testing standards. This means that, during testing, The program correctness demonstration and the
attention must be paid to much more details than it programming of correct programs are two similar
is listed in specification itself. Due to lack of time theoretical problems, which are very meaningful in
or money, only parts of the software are being practice [11]. The first is resolved within the
tested, or the parts listed in specification. program analysis and the second within the
Structural testing method belongs to another program synthesis, although because of the
strategy of testing approaches, so-called "white connection that exists between the program analysis
box"" (some authors call it transparent or glass and the program synthesis it is noticed the
box). Criterion of usual "white box" is to execute reciprocal interference of the two processes.
every executive statement during the testing and to Nevertheless, when it is a mater of the automatic
write every result during testing in a testing log. methods that are to prove the correctness and of the
The basic force in all these testings is that complete
code is taken into account during testing, which
makes easier to find errors, even when software 1
details are unclear or incomplete. McCabe, measure based on a number and
structure of the cycle.

UbiCC Journal Volume 4 No. 3 619

Special Issue on ICIT 2009 Conference - Bioinformatics and Image

methods of automatic program synthesis, the single-dimension sequences and programs within a
difference between them is evident. Pascal program. Number of passages through cyclic
In reference [12] in describes the initial structures must be fixed in advance using counter.
possibility of automatic synthesis of simple During the testing process of given (input) Pascal
programs using the resolution procedure of program both parts are involved, transformation
automatic demonstration of theorems (ADT), more and resolution, in a following way: Transformation
precisely with the resolution procedure of part
deduction of answer to request. The demonstration ends function by a sequence of clauses, or
that the request that has a form of (x)W(x) is the demands forced termination, depending
logical consequence of the axioms that determinate on input Pascal program.
the predicate W and determinate (elementary) Impossibility of generating a sequence of clauses in
program operators provides that the variable x in transformation part points that a Pascal program has
the response obtains the value that represents the no correct syntax, i.e. that there are mistakes in
requested composition of (elementary) operators, syntax or in logical structure (destructive testing).
i.e. the requested program. The works of Z. Mann, In this case, since axiomatic base was not
observe in detail the problems of program analysis constructed, resolution part is not activated and user
and synthesis using the resolution procedure of is prompted to mend a Pascal program syntax. In
demonstration and deduction of the response. the case that transformation part finishes function
The different research tendency is axiomatic by generating a sequence of clauses, resolution part
definition of the semantics of the program language is activated with following possible outcomes:
Pascal in the form of specific rules of the program Ra) ends function giving a list of symbolic
logic deduction, described in the works [14,15]. outputs and corresponding Pascal
Although the concepts of the two mentioned program routes, or
approaches are different, they have the same Rb) ends by message that id could not generate
characteristic. It is the deductive system on list of outputs and routes, or
predicate language. In fact, it is a mater of Rc) doesn't end function and demands forced
realization in the special predicate computation that termination.
is based on deduction in formal theory. With this, Ra) By comparing symbolic outputs and routes
the problem of program correctness is to be related with specification, the user may
to automatic checkup of (existing) demonstrations declare a given Pascal program as
regarding mathematical theorems. The two correct, if outputs are in
approaches mentioned above and their accordance to specification
modifications are based on that kind of concept. (constructive testing), or
if a discrepancy of some symbolic
2. DESCRIPTION OF METHOD FOR ONE expression to specification has
PASSAGE SYMBOLIC TESTING PROGRAM been found, this means that there
is a semantic error in a Pascal
The method is based on transformation of given program (destructive testing) at the
Pascal program, into a sequence of prologue corresponding route.
clauses, which comprise axiomatic base for Rb) Impossibility to generate a list of symbolic
functioning of deductive resolution mechanism in a expressions in resolution part, which means
BASELOG system [10] . For given Pascal program, that there is a logical-structural error in a
by a single passage through resolution procedure of Pascal program (destructive testing).
BASELOG system, all possible outputs in Pascal Rc) Too long function or a (unending) cycle
program are obtained in a symbolic shape, together means that there is a logic and/or semantic
with paths leading to every one of them. Both parts, error in a Pascal program (destructive
transformation and resolution one, are completely testing).
automated and are naturally attached to each other.
When a resolution part has finished, a sequence of In this way, by using this method, user may be
paths and symbolic outputs is reading out for given assured in correctness of a Pascal program or in
input Pascal program. This is a transformation of presence of syntax and/or logic-structure semantic
programming structures and programming errors. As opposite to present methods of symbolic
operators into a sequence of clauses, being realized testing of the programs, important feature of this
by models depending on concrete programming method is single-passage, provided by specific
language. Automation covers branching IF-THEN property of OL resolution [11] with marked
and IF-THEN-ELSE structures, as well as WHILE- literals, at which a resolution module in BASELOG
DO and REPEAT UNTIL cyclic structures, system is founded.
which may be mutually nested in each other. This
paper gives review of possibilities in work with

UbiCC Journal Volume 4 No. 3 620

Special Issue on ICIT 2009 Conference - Bioinformatics and Image

3. DEDUCTION IN FORMAL THEORY AND According to The basic presumptions of

PROGRAM CORRECTNESS programming logic are given in [14]. The basic
relation {P}S{Q}is a specification for program S
The program verification may lean on with following meaning: if predicate P at input is
techniques for automatic theorem proving. These fulfilled (correct) before execution of program S,
techniques embody principles of deductive then predicate Q at the output is fulfilled (correct)
reasoning, same ones that are used by programmers after execution of program S. In order to prove
during program designation. Why not use same correctness of program S, it is necessary to prove
principles in the automatic synthesis system, which relation {P}S{Q}, where input values of variables
may construct program instead of merely proving must fulfill predicate P and output variable values
its correctness? Designing the program demands must fulfill predicate Q. Since it is not proven that
more originality and more creativity than proving S is terminating, and that this is only presumption,
its correctness, but both tasks demand the same way then we may say that partial correctness of the
of thinking. [13] program is defined. If it is proven that S terminates
Structural programming itself helped the and that relation {P}S{Q} is fulfilled, we say that S
automatic synthesis of computer programs in the is completely correct. For program design, we use
beginning, establishing principles in program thus determined notion of correctness.
development on the basis of specification. These The basic idea is that program design should be
principles should be guidelines for programmers. In done simultaneously with proving correctness of
the matter of fact, advocates of structural the program for given specifications[15,16]. First
programming were very pessimistic regarding the specification {P}S{Q} is executed with given
possibility to ever automatize their techniques. prerequisite P and given resultant post condition Q,
Dijkstra went so far to say that we should not and then subspecifications of {Pi}Si{Qi} type are
automatize programming even if we could, since executed for components Si from which the
this would deprive this job from all delight. program S is built. Special rules of execution
Proving program correctness is a theoretical provide proof that fulfillment of relation {P}S{Q}
problem with much practical importance, and is follows from fulfillment of relations {Pi}Si{Qi} for
done within program analyse. Related theoretical component programs Si.
problem is the design of correct programs that is Notice that given rules in [9] are used for
solved in another way within program synthesis. manual design and manual confirmation of
It is evident that these processes are intertwined, program's correctness, without mention about
since analysis and synthesis of programs are closely possibility of automatic (resolution) confirmation
related. Nevertheless, differences between these methods.If we wish to prove correctness of
problems are distinct regarding automatic method program S, we must prove relation {P}S{Q}, where
of proving program correctness and automatic input values of variables must fulfill the formula P
method of program synthesis. and output values of variables must fulfill the
If we observe a program, it raises question of formula Q. This defines only partial correctness of
termination and correctness, and if we observe two program S, since it is assumed that program S
programs we have question of equivalence of given terminates. If we prove that S terminates and that
programs. Abstract, i.e. non-interpreted program is relation {P}S{Q} is satisfied, we say that S is
defined using pointed graph. From such a program, totally correct.Thus designated principle of
we may obtain partially interpreted program, using correctness is used for program designation.
interpretation of function symbols, predicate Designation starts from specification {P}S{Q} with
symbols and constant symbols. If we interpret free given precondition P and given resulting
variables into partially interpreted program, a postcondition Q.Formula {P}S{Q} is written as
realized program is obtained. Function of such a K(P, S, Q), where K is a predicate symbol and
program is observed using sequence executed. P,S,Q are variables of first-order predicate
Realized program, regarded as deterministic, has calculation.
one executive sequence, and if it does not exist at {Pzy} z := y {P}
all, it has no executive sequence. On the other hand,
when the program is partially interpreted, we see we are writing as K(t(P,Z,Y), d(Z,Y), P)...
several executive sequences. In previously stated where t,d are function symbols and P,Z,Y are
program type, for every predicate interpreted it is variables;
known when it is correct and when not, which
...Rules R():
would mean that depending on input variables
different execution paths are possible. Considering P1. . {P}S{R} , RQ.
abstract program, we conclude that it has only one
executive sequence, where it is not known whether {P}S{Q}.
predicate P or his negation is correct. we write.. K(P,S,R) Im(R,Q) K(P,S,Q)

UbiCC Journal Volume 4 No. 3 621

Special Issue on ICIT 2009 Conference - Bioinformatics and Image

where Im (implication) is a predicate symbol, and A(S) = R() A(). This means that derivation of
P, S, R, Q are variables; theorem B within theory could be replaced with
derivation within special predicate calculus S,
P2 RP, {P}S{Q}
whose own axioms A(S)= R() A().Axioms of
{R}S{Q}. we write Im(R,P) K(P,S,Q) special predicate calculus S are: A(S)= A()
K(R,S,Q) R().We assume that s is a syntax unit whose
P3 {P}S1{R} , {R}S2{Q} (partial) correctness is being proven for certain
input predicate U and output predicate V.
{P}begin S1; S2 end {Q}
Within theory S is being proved
K(P,S1,R) K(R,S2,Q) K(P,s(S1,S2),Q)
where s is a function symbol, and P, S1, S2, R, q ... (P)(Q)K(P,s,Q)
are variables S
where s is a constant for presentation of a given
P4 {PB}S1{Q, {P~B}S2{Q} program. Program is written in functional notation
{P}if B then S1 else S2{Q} with symbols: s (sequence), d (assigning), ife (if-
then-else), if (if-then), wh (while), ru (repeat-until).
K(k(P,B),S1,Q)K(k(P,n(B)),S2,Q) To starting set of axioms A(S), negation of
K(P,ife(B,S1,S2),Q) statement is added: Result of negation using
where k, n, ife are function symbols resolution procedure is as follows: /Im(X,Y,)
Odgovor(P,Q), where X,Y,P,Q are values for
P5 {PB}S{Q} , P~B Q which successful negation To means that for these
values a proof is found. But this does not mean that
{P} if B then S{Q}
given program is partially correct. It is necessary to
K(k(P,B),S,Q) Im(k(P,n(B)),Q) establish that input and output predicates U, V are
K(P,if(B,S),Q) in accordance with P, Q, and also that Im (X,Y)
is really fulfilled for domain predicates ant
where k, n, if are function symbols
terms.Accordance means confirmation that .. is
P6 {PB} S {P } valid. : U P, Q V) ( X Y).there
are two ways to establish accordance: manually or
{P} while B do S {P~B} by automatic resolution procedure. Realization of
K(k(P,B),S,P) K(P,wh(B,S),k(P,n(B))) these ways is not possible within theory S, but it is
possible within the new theory, which is defined by
where k, n, wh are function symbols predicates and terms which are part of the program
s and input-output predicates U, V. Within this
P7 {P}S{Q} , Q~B P theory U, P, Q, V, X, Y are not variables, but
formulae with domain variables, domain terms and
{P}repeat S until B {QB} domain predicates.This method concerns derivation
within special predicate calculus based on
K(P,S,Q) Im(k(Q,n(B)),P) deduction within the formal theory. Thus the
K(P,ru(S,B),k(Q,B)) program's correctness problem is associated with
where k, n, ru are function symbols automatic proving of (existing) proofs of
mathematical theorems.
Transcription of other programming logic rules is
The formal theory is determined with the
also possible.
formulation of (S(), F(), A(), R()) where S is
the set of symbols (alphabet) of the theory , F is
Axiom A():
A1 K(t(P,Z,Y),d(Z.Y),P) the set of formulas (regular words in the alphabet
assigning axiom S), A is the set of axioms of the theory (AF), R
Formal theory is given by ((), F(), A(), R()), is the set of rules of execution of the theory .
where is a set of symbols (alphabet) of theory , Deduction (proof) of the formula B in the theory
F is a set of formulae (correct words in alphabet ), is the final sequence B1, B2, ... , Bn (Bn is B) of
A is a set of axioms for theory (AF), R is a set of formulas of this theory, of that kind that for every
derivation rules for theory .B is a theorem within element Bi of that sequence it is valid: Bi is axiom,
theory if and only if B is possible to derive within or Bi is deducted with the application of some rules
calculus k from set R() A() (k is a first-order of deduction RiR from some preceding elements
predicate calculus).Let S be special predicate
calculus (first-order theory) with it's own axioms

UbiCC Journal Volume 4 No. 3 622

Special Issue on ICIT 2009 Conference - Bioinformatics and Image

of that sequence. It is said that B is the theorem of Regarding technique of automatic theorems
the theory and we write B [17]. proving, most investigations have been done in
resolution rules of derivation. Resolution is a very
important derivation rule with completeness
Suppose S() is a set of symbols of predicate property.
computation and F() set of formulas of predicate
computation. In that case, the rules of deduction R( Demonstrate that the mentioned sequence is
) can be written in the form: Bi1Bi2 ... Bik deduction of formula B in theory.
Bi (Ri) where Bik, Bi are formulas from F().
One way of solving this problem is to verify
Suppose predicate computation of first line, than
that the given sequence corresponds to definition of
it is valid:
deduction in theory. The other way is to use (1),
i.e. (2):
R(), A() B if B (1) If we demonstrate that

R(), A() B B2 ... Bn (3)
B is theorem in the theory if and only if B is
deductible in computation from the set R()
A(). that is sufficient for conclusion that B1, B2, ... , Bn
is deduction in .
Suppose S is a special predicate computation
(theory of first line) with its own axioms: And also it is sufficient to demonstrate that R(),
A(S) = R() A() , (rules of deduction in S are
A() Bi , for i = 1,2,...,n, with this it is
rules of deduction of computation ) then it is valid
A(S) B if B , so that (1) can be written: demonstrated (3).
S Demonstration for (3) can be deducted with the
resolution invalidation of the set
R()A(){~B1~B2 ... ~Bn}, or with n
B if B (2)
S invalidations of sets R()A(){~Bi}.

That means that the deduction of theorem B in Notice that for the conclusion that B1, B2, ..., Bn is
theory can be replaced with deduction in special deduction in it is not enough to demonstrate R(),
predicate computation S, that has its own axioms A() (B1 B 2 ... Bn - 1 Bn ) ,i.e. it is
A(S) = R() A().
Now we can formulate the following task: not enough to realize resolution invalidation of the
set R()A(){B1, B2, ... , Bn-1}{~Bn},
The sequence of formulas has been given B1, B2, ... because this demonstrate only that Bn is deductible
, Bn (Bn is B, Bi different from B for i<n) of theory
in supposing that in is deductible B1B2...
. Bn-1 .
Implementation of programs for proving Always when B1, B2, ..., Bn is really deduction
theorems was in the beginning only in mathematics
area. When it was seen that other problems could in , (B1B2...Bn-1 Bn) will be correct, but
be presented as possible theorems which need to be vice versa is not always valid. It can happen that
proven, application possibilities were found for (B1B2...Bn-1 Bn) is deductible in , but
areas as program correctness, program generating, that B1B2...Bn-1 is not deductible in , (see
question languages over relation databases, example 1).
electronic circuits design.
And also, the demonstration for R(), A()
As for formal presentation where theorem is
being proven, it could be statement calculus, first-
order predicate calculus, as well as higher-order Bn , that can be realized with resolution
logic. Theorems in statement calculus are simple
for contemporary provers, but statement calculus is invalidation of the set R()A(){~Bn}, means
not expressional enough. Higher-order logic is that Bn is theorem in , i.e. that Bn is deductible in
extremely expressional, but they have a number of
practical problems. Therefore a first-order predicate , but this is not enough for the conclusion that B1,
calculus is probably the most used one. B2, ..., Bn is deduction in (except for the case that

UbiCC Journal Volume 4 No. 3 623

Special Issue on ICIT 2009 Conference - Bioinformatics and Image

in the invalidation appears invalidation of each Bi, 7.sode, 1.lateral :

see example 1). =(S(2),3)&
Finally, here it is necessary to underline that not LEVEL=5;resolvent:
correspondence to set R()A(){~Bn} does not ~r(3,1)~r(4,2)/~r(5,3)~r(X1,2)~=(S(X1),5)&
mean not correspondence to formula ~Bn as it is, 9.side, 1.lateral :
=(S(4),5)&
but only in the presence of R()A().
LEVEL= 6; resolvent:
~r(3,1)~r(4,2)&
Example 1. Suppose A() is: {r(1,1), r(1,3)} and R( 4.side, 4.lateral :
) contains three rules of deduction: ~r(X1,Y1)~=(S(X1),U1)~=(S(Y1),V1)r(U1,V1)&
:r(m,n)r(n,m); : r(m,n)r(m+1,n+1) ; LEVEL= 7; resolvent:
:r(m,n)r(n,p)r(n,p)
symmetry correspondence with the next one ~r(3,1)/~r(4,2)~r(X1,Y1)~=(S(X1),4)~=(S(Y1),2)&
transitivity 6.side, 1.lateral :
Demonstrate that the sequence J is: r(3,1), r(4,2), =(S(1),2)&
r(5,3), r(5,1) , r is predicate symbol, one correct LEVEL= 8; resolvent:
deduction of formula r(5,1) in theory .
~r(3,1)/~r(4,2)~r(X1,1)~=(S(X1),4)&
8.side, 1.lateral :
It is sufficient to demonstrate:
=(S(3),4)&
{,,}, A() J . LEVEL= 9; resolvent:
~r(3,1)&
In the next demonstration x+1 is signed with 2.side, 1.lateral :
S(x) and axioms for the next one are added: r(3,1)&
LEVEL= 10; resolvent:
1 &
~r(3,1)~r(4,2)~r(5,3)~r(5,1)& DEMONSTRATION IS PRINTED
9 Example 2
r(1,1)& begin
r(3,1)& p:=x;
~r(X1,Y1)r(Y1,X1)& i:=0;
~r(X1,Y1)~=(S(X1),U1)~=(S(Y1),V1)r(U1,V1)& while i<=n do
~r(X1,Y1)~r(Y1,Z1)r(X1,Z1)& begin
=(S(1),2)& i:=i+1;
=(S(2),3)& p:=p*i;
=(S(3),4)& end;
=(S(4),5)& end.
Demonstration with invalidation: Given program is written:
number of generated resolvents = 934 s(s(d(p,x),d(i,0)),w(i<=n,s(d(i,i+1),d(p,p*i))))
maximum level = 10 Constant b is a mark for predicate i<=n
DEMONSTRATION IS PRINTED constant t1 is i+1, constant t2 is term p*i
level on which empty composition is generated = thus we obtain
10 s(s(d(p,x),d(i,0)),w(b,s(d(i,t1),d(p,t2))))
LEVEL=1; central composition
:~r(3,1)~r(4,2)~r(5,3)~r(5,1)& 1
5.side, 3.lateral : /O(X1,V1)~K(X1,s(h,g),Y1)~K(Y1,w(b,s(d(i,t1),d(
~r(X1,Y1)~r(Y1,Z1)r(X1,Z1)& p,t2))),V1)&
LEVEL= 2; resolvent: 8
~r(3,1)~r(4,2)~r(5,3)/~r(5,1)~r(5,Y1)~r(Y1,1)& ~K(Y1,d(p,x),V1)K(Y1,h,V1)& /reserve for
2.side, 1.lateral : shortening the note
r(3,1)& ~K(Y1,d(i,0),V1)K(Y1,g,V1)& /reserve for
LEVEL= 3; resolvent: shortening the note
~r(3,1)~r(4,2)~r(5,3)& ~K(X1,Y1,U1)~K(U1,Y2,V1)K(X1,s(Y1,Y2),V1)
4.side, 4.lateral : & /sequence rule
~K(k(X1,V2),U0,X1)K(X1,w(V2,U0),k(X1,ng(V2)
~r(X1,Y1)~=(S(X1),U1)~=(S(Y1),V1)r(U1,V1)& ))& /rule for while
LEVEL= 4; resolvent: K(t(X1,Z1,Y1),d(Z1,Y1),X1)& /assigning axiome
~r(3,1)~r(4,2)/~r(5,3)~r(X1,Y1)~=(S(X1),5)~= ~IM(X2,Y1)~K(Y1,U0,V1)K(X2,U0,V1)&
(S(Y1),3)& /consequence rule

UbiCC Journal Volume 4 No. 3 624

Special Issue on ICIT 2009 Conference - Bioinformatics and Image

~IM(Y1,V1)~K(X1,U0,Y1)K(X1,U0,V1)& /
consequence rule /~IM(k(V1,b),t(t(V1,p,t2),i,t1))/O(X2,k(V1,ng(b)))/
~O(X1,V1)& / negation addition ~K(X2,s(h,g),V1)~K(X2,h,U1)~K(U1,g,V1)&
0 2.lateral, 2.literal :
0 ~K(Y1,d(i,0),V1)K(Y1,g,V1)&
LEVEL= 8; resolvent:
LP system generates next negation
number of resolvents generated = 10 /~IM(k(V0,b),t(t(V0,p,t2),i,t1))/O(X2,k(V0,ng(b)))/
maximal obtained level = 11 ~K(X2,s(h,g),V0)~K(X2,h,Y1)/~K(Y1,g,V0)~K(Y
DEMONSTRATION IS PRINTED 1,d(i,0),V0)&
level where the empty item is generated = 11 5.lateral, 1.literal :
LEVEL=1; central item K(t(X1,Z1,Y1),d(Z1,Y1),X1)&
:/O(X1,V1)~K(X1,s(h,g),Y1)~K(Y1,w(b,s(d(i,t1),d LEVEL= 9; resolvent:
(p,t2))),V1)&
4.lateral, 2.literal : /~IM(k(X1,b),t(t(X1,p,t2),i,t1))/O(X2,k(X1,ng(b)))/
~K(X2,s(h,g),X1)~K(X2,h,t(X1,i,0))&
~K(k(X1,V2),U0,X1)K(X1,w(V2,U0),k(X1,ng(V2) 1 lateral, 2.literal :
))& ~K(Y1,d(p,x),V1)K(Y1,h,V1)&
LEVEL= 2; resolvent: LEVEL= 10; resolvent:

/O(X1,k(X0,ng(b)))~K(X1,s(h,g),X0)/~K(X0,w(b,s /~IM(k(X1,b),t(t(X1,p,t2),i,t1))/O(Y1,k(X1,ng(b)))/
(d(i,t1),d(p,t2))),k(X0,ng(b)))~K(k(X0,b),s(d(i,t1),d ~K(Y1,s(h,g),X1)/~K(Y1,h,t(X1,i,0))~K(Y1,d(p,x),
(p,t2)),X0)& t(X1,i,0))&
3.lateral, 3.literal : 5.lateras, 1.literal :
K(t(X1,Z1,Y1),d(Z1,Y1),X1)&
~K(X1,Y1,U1)~K(U1,Y2,V1)K(X1,s(Y1,Y2),V1) LEVEL= 11; resolvent:
& /O(Y1,k(X1,ng(b)))/~K(Y1,s(h,g),X1)/~K(Y1,h,t(X
LEVEL= 3; resolvent: 1,i,0))~K(Y1,d(p,x),t(X1,i,0))&
5. lateral, 1.literal :
/O(X1,k(V1,ng(b)))~K(X1,s(h,g),V1)/~K(V1,w(b,s K(t(X1,Z1,Y1),d(Z1,Y1),X1)&
(d(i,t1),d(p,t2))),k(V1,ng(b)))/~K(k(V1,b),s(d(i,t1), LEVEL= 11; resolvent:
d(p,t2)),V1)~K(k(V1,b),d(i,t1),U1)~K(U1,d(p,t2),V DEMONSTRATION IS PRINTED
1)& Now we need to prove compliance, i.e. that there is
5.lateral, 1.literal : in effect:
K(t(X1,Z1,Y1),d(Z1,Y1),X1)& ( X YZT ) (U P, Q V) that is at
LEVEL= 4; resolvent: LEVEL= 12; resolvent:
/IM(k(X1,b),t(t(X1,i,t1),p,t2))O(t(t(X1,i,0),p,x),k(X
/O(X1,k(X0,ng(b)))~K(X1,s(h,g),X0)/~K(X0,w(b,s 1,ng(b)))&
(d(i,t1),d(p,t2))),k(X0,ng(b)))/~K(k(X0,b),s(d(i,t1), By getting marks to domain level we obtain:
d(p,t2)),X0)~K(k(X0,b),d(i,t1),t(X0,p,t2))& (X1 (i<=n) X1ii+1 pp/i)i (UX1i 0 px) (X1

6.lateral, 3.literal : (i<=n) V)7
~IM(X2,Y1)~K(Y1,U0,V1)K(X2,U0,V1)& i
LEVEL= 5; resolvent: Putting X1: p = x ( j 1) we obtain
j =0
/O(X1,k(X0,ng(b)))~K(X1,s(h,g),X0)/~K(X0,w(b,s following correct implications:
(d(i,t1),d(p,t2))),k(X0,ng(b)))/~K(k(X0,b),s(d(i,t1),
d(p,t2)),X0)/~K(k(X0,b),d(i,t1),t(X0,p,t2))~IM(k(X
0,b),Y1)~K(Y1,d(i,t1),t(X0,p,t2))&
5. lateral, 1.literal :
K(t(X1,Z1,Y1),d(Z1,Y1),X1)&
LEVEL= 6; resolvent:

/~IM(k(X0,b),t(t(X0,p,t2),i,t1))/O(X1,k(X0,ng(b)))
~K(X1,s(h,g),X0)&
3.lateral, 3.literal :

~K(X1,Y1,U1)~K(U1,Y2,V1)K(X1,s(Y1,Y2),V1)
&
LEVEL= 7; resolvent:

UbiCC Journal Volume 4 No. 3 625

Special Issue on ICIT 2009 Conference - Bioinformatics and Image

i program development. Software producers would

p = x ( j 1) => like to predict number of errors in software systems
j =0 before the application, so they could estimate
i quality of product bought and difficulties in
p i = x i ( j 1) => maintenance process [18]. Testing often takes 40%
j =0 of time needed for development of software
i package, which is the best proof that it is a very
p i = x (i 1 + 1) ( j 1) => complex process. Aim of testing is to establish
j =0
whether software is behaving in the way envisaged
by specification. Therefore, primary goal of
i +1
p i = x ( j 1)
software testing is to find errors. Nevertheless, not
all errors are ever found, but there is a secondary
j =0
goal in testing, that is to enable a person who
performs testing (tester) to trust the software system
For i = 0 we obtain: [19]. From these reasons, it is very important to
i choose such a testing method that will, in given
p = x ( j 1) => functions of software system, find those fatal errors
j =0 that bring to highest hazards. In order to realize
0
this, one of tasks given to programmers is to
p = x ( j 1) => develop software that is easy to test ("software is
j =0
designed for people, not for machines") [20].
Program testing is often equalized to looking for
p=x any errors [20]. There is no point in testing for
errors that probably do not exist. It is much more
By this the compliance is proven, which is enough efficient to think thoroughly about kind of errors
to conclude that a given program is (partially) that are most probable (or most harmful) and then
correct (until terminating). to choose testing methods that will be able to find
such errors. Success of a set of test items is equal to
5. INTERPRETATION RELATED TO successful execution of detailed test program. One
DEMONSTRATION OF PROGRAM of big issues in program testing is the error
CORRECTNESS reproduction (testers find errors and programmers
remove bugs) [21]. It is obvious that there must be
Interpret the sequence J: B1, ... , Bn as program some coordination between testers and
S. Interpret the elements A() as initial elements for programmers. Error reproduction is the case when
the composition of program S, and the elements R( it would be the vest to do a problematic test again
and to know exactly when and where error
) as rules for the composition of program occurred. Therefore, there is no ideal test, as well as
constructions. there is no ideal product.[22] .Software producers
Vice versa, if we consider program S as would like to anticipate the number of errors in
sequence J, initial elementary program operators as software systems before their application in order to
elements A() and rules for composition of estimate the quality of acquired program and the
program structures as elements R(), with this the difficulties in the maintenance. This work gives the
problem of verification of the correctness of the summary and describes the process of program
given program is related to demonstration of testing, the problems that are to be resolved by
correctness of deduction in corresponding formal testers and some solutions for the efficacious
theory. It is necessary to represent axioms, rules elimination of errors[23]. The testing of big and
and program with predicate formulas. complex programs is in general the complicated
With all that is mentioned above we defined the process that has to be realized as systematically as
general frame for the composition of concrete possible, in order to provide adequate confidence
proceedings for demonstration of program and to confirm the quality of given application [24].
correctness with the deductive method. With the The deductions in formal theories represent general
variety of choices regarding axioms, rules and frame for the development of deductive methods
predicate registration for the different composition for the verification of program correctness. This
proceedings are possible. frame gives two basic methods (invalidation of
added predicate formula and usage of rules of
program logic) and their modifications.
6. CONCLUSION The work with formula that is added to the
given program implies the presence of added
Software testing is the important step in axioms and without them, the invalidation cannot

UbiCC Journal Volume 4 No. 3 626

Special Issue on ICIT 2009 Conference - Bioinformatics and Image

be realized. The added axioms describe [15] Hoare C.A.R. Proof of a program Find
characteristics of domain predicates and operations Communications of the ACM 14, 39-45.
and represent necessary knowledge that is to be 1971.
communicated to the deductive system. The [16] Hoare C.A.R, Wirth N., An axiomatic
existing results described above imply that kind of definition of the programming language
knowledge, but this appears to be notable difficulty Pascal , Acta Informatica 2, pp. 335-355.
in practice. 1983
[17] Markoski B., Hotomski P., Malbaski D.,
ACKNOWELDGEMENTS Obradovic D. Resolution methods in proving
The work presented in the paper was developed the program correctness , YUGER, An
within the IT Project WEB international journal dealing with theoretical
portals for data analysis and consulting, No. and computational aspects of operations
13013, supported by the research, systems science and menagement
government of Republic of Serbia, 2008. 2010. science, Beograd, Serbia, 2007,
[18] Myers G.J., The Art of Software Testing, New
7. REFERENCES York , Wiley, 1979.
[19] Chan, F., T. Chen, I. Mak and Y. Yu,
[1] Marks, David M. Testing very big systems Proportional sampling strategy: Guidelines
New York:McGraw-Hill, 1992 for software test practitioners , Information
[2] Manthos A., Vasilis C., Kostis D. and Software Technology, Vol. 38, No. 12,
Systematicaly Testing a Real-Time Operating pp. 775-782, 1996.
System IEEE Trans. Software Eng., 1995 [20] K. Beck, Test Driven Development: By
[3] Voas J., Miller W. Software Testability: The Example, Addison-Wesley, 2003
New Verification IEEE Software 1995 [21] P. Runeson, C. Andersson, and M. Hst, Test
[4] Perry William E. Year 2000 Software Testing Processes in Software Product EvolutionA
New York: John Wiley& SONS 1999 Qualitative Survey on the State of Practice,
[5] Whittaker J.A., Whittaker, Agrawal K. J. Software Maintenance and Evolution, vol.
A case study in software reliability 15, no. 1, 2003, pp. 4159.
measurement Proceedinga of Quality Week, [22] G. Rothermel et al., On Test Suite
paper no.2A2, San Francisko, USA 1995 Composition and Cost-Effective Regression
[6] Zeller A. Yesterday, my program worked, Testing, ACM Trans. Software Eng. and
Today, it does not. Why?Passau Germany, Methodology, vol. 13, no. 3, 2004, pp. 27733
2000 [23] N. Tillmann and W. Schulte, Parameterized
[7] Markoski B., Hotomski P., Malbaski D., Unit Tests, Proc. 10th European Software
Bogicevic N. Testing the integration and the Eng. Conf., ACM Press, 2005, pp. 253262.
system, International ZEMAK symposium, [24] Nathaniel Charlton Program verification
Ohrid, FR Macedonia, 2004. with interacting analysis plugins Formal
[8] McCabe, Thomas J, &Butler, Charles W. Aspects of Computing. London: Aug 2007.
Design Complexity Measurement and Testing Vol. 19, Iss. 3; p. 375
Communications of the ACM 32, 1992
[9] Markoski B., Hotomski P., Malbaski D.
Testing the complex software, International
ZEMAK symposium, Ohrid, FR Macedonia,
2004.
[10] Chidamber, S. and C. Kemerer, Towards a
Metrics Suite for Object Oriented Designe,
Proceedings of OOPSLA, July 2001
[11] J.A. Whittaker, What is Software Testing?
And Why Is It So Hard? IEEE Software, vol.
17, no. 1, 2000,
[12] Nilsson N., Problem-Solving Methods in
Artificial Intelligence , McGraw-Hill, 1980
[13] Manna Z., Mathematical Theory of
Computation , McGraw-Hill, 1978
[14] Floyd. R.W., Assigning meanings to
programs , In: Proc. Sym. in Applied
Math.Vol.19, Mathematical Aspects of
Computer Science, Amer. Math. Soc., pp. 19-
32., 1980.

UbiCC Journal Volume 4 No. 3 627