Indeed, but as far as I can tell, the particular specification language here is at a much lower level of abstraction, one where we have only slightly-abstracted

Indeed, but as far as I can tell, the particular specification language here is at a much lower level of abstraction, one where we have only slightly-abstracted pointers, and consequently, I suspect, a specification using this particular logic will have no choice but to say how to generate X (or perhaps I should say that the intention is that one should say how to generate X, even if, formally, one can avoid doing so.)