Joshua, this is a research question! To the best of my knowledge, currently and in practice, developers use steamroller tactics to check postconditions. The standard way to verify that the LHC works as intended, in a method
exterminate on a class EarthPopulation:exterminate
| oldSize |
oldSize := self size.
LHC switchOn.
self size should < oldSize.
That is, you copy whatever you intend to change and then compare new with old value. It isn’t difficult to imagine that this can lead to trouble if whatever you want to change isn’t cloneable. And of course it isn't possible to switch off the overhead of these assertions.* And that’s where Histoory (by Pluquet et al) comes to the rescue. Not only does it work independent of the cloneability, it also provides a much cleaner syntax:
exterminate
[LHC swithOn]
postCond: [:old | old size should < self size]
Alas, it isn’t in the latest flavor of any programming language, so I truly hope that Histoory will make it into Pharo :).
* I added this sentence after Joshua's correct observation of this problem.