# What is the intuitive meaning of the weakest precondition expression $\text{wp}(S,R)$ in refinement calculus with miracles?

What is the intuitive meaning of the expression $$\text{wp}(S,R)$$ ($$\text{wp}$$ = weakest precondition) in refinement calculus with miracles?

When the $$\text{wp}$$ function describes partial correctness (as in Hoare's calculus), $$\text{wp}(S,R)$$ means intuitively: if you start at a state satisfying $$\text{wp}(S,R)$$ and then proceed to execute the program $$S$$, then, if the computation terminates, the final state will satisfy $$R$$.

When the $$\text{wp}$$ function describes total correctness (as in Dijkstra's calculus), $$\text{wp}(S,R)$$ means intuitively: if you start at a state satisfying $$\text{wp}(S,R)$$ and then proceed to execute the program $$S$$, then the computation is guaranteed to terminate in a state satisfying $$R$$.

But what is the intuitive meaning of $$\text{wp}(S,R)$$ in refinement calculus with "miracles" (as in Carroll Morgan's textbook Programming from Specifications)? For instance, how should I understand the fact that $$\text{wp}(S, \text{false}) = \text{true}$$ when $$S$$ is the specification statement $$x:[\text{true},\text{false}]$$? Is it simply partial correctness? If so, then why introduce the concept of "miracles", and not just call it "partial correctness"?