Formal program reversing by conditioned slicing

In (Oliveira and Villavicencio, 2001) we have applied [P]=([P₁], ..., [P_n]) as a conjuncture to reverse calculate the formal specifications of a program P through the application of static slicing on output variables. This conjecture defines a calculation pattern: the formal specification for each slice is calculated and the whole program specification is obtained by combining the slice specifications by the split (<...>) combinator. However, the conjecture fails when we use conditioned slices as a complexity-reduction mechanism. Thus, it is necessary to define a new calculation pattern for the conditioned slices. Since we need to reconstruct the static slice on an output variable combining the conditioned slices on such variable, "transversal calculus" is required instead of a "linear calculation" as in (Oliveira and Villavicencio, 2001). The definition of the calculus patterns is important when facing the construction of the automatic support for the present approach because they contribute to the systematization of the calculus process.