A Logical Framework for Software Testing

Summary form only given. In software testing, when testing samples contradict the specification of a software system, the best way to locate the error-making commands is logical reasoning; therefore a formal logical reasoning system might be developed for making revision of software systems. In this paper, a formal system, called R-calculus, is introduced in first order languages. It is used to spot those error-making commands which cause the contradiction to the testing example. Therefore, R-calculus helps a great deal to revise the software system. The basic form of R-calculus is a pair in which the first part is a consistent set of formulas specifying the results of the testing samples, while the second part is a specification that contradicts the first part. R-calculus consists of a set of R-rules and each R-rule is designed for one logical connective symbol or one quantifier symbol occurring in the specification. Some examples are given to demonstrate how to use the R-calculus. It is proved that R-calculus is sound and complete. A testing theorem is further proved. The theorem says that R-calculus can deduce formally all possible revisions for a specification that contradicts testing samples. It further says that some software tools can be designed and implemented on computers to revise software systems interactively with the testing engineers.