1
$\begingroup$

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"?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.