On one application of computations with oracle
Alexei Lisitsa, Andrei P. Nemytykh · Programming and Computer Software · 2010
Let P(d) be a program implementing a partial recursive function φ. Let $$ \mathcal{O} $$ P denote a function defined on the domain of function φ that maps an input data d 0 onto the path of computation of P on the input d 0. Let Q(p, d) be a program returning a value if and only if p = $$ \mathcal{O} $$ P (d), and let the value of the program be Q( $$ \mathcal{O} $$ P (d), d) = P(d). Program Q(p, d), which is totally absurd from the point of view of its practical computation on concrete input data, may be practically useful when it is analyzed by a metaprogram. It is shown in the paper how program Q(p, d) can be used for verification of a postcondition imposed on program P(d). The proposed method was tested on verification tasks for cache coherence protocols and other distributed computing systems.