Resolution method for one passage symbolic testing of ramified program structures

摘要

One of oldest and best-known methods used in constructive testing of smaller programs is the symbolic program execution. It is partly similar to method of simulation of computer function, but differs in aim. One of ways to prove whether given program is written correctly is to execute it symbolically. Aim of this paper is to test ramified program structure using single symbolic set of inputs, in one passage through resolution procedure, by obtaining all possible outputs from program tested. 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. In transformation part models for translation of ramified structures into a declarative shapes of clause sequence were described, as well as program implementation of these transformations for Pascal programs. Obtained clause sequence is the input in resolution part in BASELOG system. Single-passage of a procedure is justified, based on OL-resolution with marked literals, which within BASELOG system gives all possible outputs in symbolic form, together with paths leading to them. Illustrative examples are given, being realized in prolog-like LP-language, with no restrictions to Horn's clauses and without final failure. It is shown how the Pascal-program is being executed into proffer of LP-system.