F*, a dependently typed dialect of ML, includes an update/select
theory of heaps and requires explicit annotations summarizing the heap
effects of a method
[1]}, [2]}, [3]}.
This approach enables modular reasoning and precise specification of
pre- and post-conditions with respect to the heap, but precludes full automation.
