%0 Journal Article
%T Resolution methods in proving the program correctness
%A Markoski Branko
%A Hotomski Petar
%A Malba£¿ki Du£¿an
%A Obradovi£¿ Danilo
%J Yugoslav Journal of Operations Research
%D 2007
%I University of Belgrade
%R 10.2298/yjor0702275m
%X 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.
%K test
%K specification
%K resolution
%K program correctness
%U http://www.doiserbia.nb.rs/img/doi/0354-0243/2007/0354-02430702275M.pdf