Reasoning about iterators with separation logic
Neelakantan R. Krishnaswami · 2006
Separation logic is an extension of Hoare logic which permits reasoning about imperative programs that use shared mutable heap structure. In this note, we show how to use higher-order separation logic to reason abstractly about an iterator protocol.