By no means I want to exclude the employment of action refinement as a `how'-step, admitting correctness proofs. However, this requires the classification of the refined action as `internal' and falls outside the scope of this thesis. Doing so may also be a reason to give up the convention adopted above. This would give rise to a completely different theory.
In Rensink: Models and Methods for Action Refinement, Ph.D. Thesis, University of Twente, 1993, a mode of action refinement is proposed that I would classify as a combined `what'- and `how'-step. Correctness proofs of the `how'-component of such a refinement step are possible, but relative to a preorder that is explicitly parametrized with the `what'-component of the refinement step.