Geodesic
Resolution Methods in Proving the Program Correctness
Yugoslav journal of operations research, Tome 17 (2007) no. 2, p. 275 .

Voir la notice de l'article provenant de la source eLibrary of Mathematical Institute of the Serbian Academy of Sciences and Arts

Program testing determines whether its behavior matches the specification, and also how it behaves in different exploitation conditions. Proving of program correctness is reduced to finding a proof for assertion that given sequence of formulas represents derivation within a formal theory of special predicted calculus. A well-known variant of this conception is described: correctness based on programming logic rules. It is shown that programming logic rules may be used in automatic resolution procedure. Illustrative examples are given, realized in prolog-like LP-language (with no restrictions to Horn's clauses and without the final failure). Basic information on LP-language are also given. It has been shown how a Pascal-program is being executed in LP-system proffer.
Classification : 68N30 03B70
Keywords: Test, specification, resolution, program correctness. 
@article{YJOR_2007_17_2_a9,
     author = {Branko Markoski and Petar Hotomski and Du\v{s}an Malba\v{s}ki and Danilo Obradovi\'c},
     title = {Resolution {Methods} in {Proving} the {Program} {Correctness}},
     journal = {Yugoslav journal of operations research},
     pages = {275 },
     publisher = {mathdoc},
     volume = {17},
     number = {2},
     year = {2007},
     zbl = {1164.68002},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/YJOR_2007_17_2_a9/}
}
TY  - JOUR
AU  - Branko Markoski
AU  - Petar Hotomski
AU  - Dušan Malbaški
AU  - Danilo Obradović
TI  - Resolution Methods in Proving the Program Correctness
JO  - Yugoslav journal of operations research
PY  - 2007
SP  - 275 
VL  - 17
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/YJOR_2007_17_2_a9/
LA  - en
ID  - YJOR_2007_17_2_a9
ER  - 
%0 Journal Article
%A Branko Markoski
%A Petar Hotomski
%A Dušan Malbaški
%A Danilo Obradović
%T Resolution Methods in Proving the Program Correctness
%J Yugoslav journal of operations research
%D 2007
%P 275 
%V 17
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/YJOR_2007_17_2_a9/
%G en
%F YJOR_2007_17_2_a9
Branko Markoski; Petar Hotomski; Dušan Malbaški; Danilo Obradović. Resolution Methods in Proving the Program Correctness. Yugoslav journal of operations research, Tome 17 (2007) no. 2, p. 275 . http://geodesic.mathdoc.fr/item/YJOR_2007_17_2_a9/