BI as an Assertion Language for Mutable Data Structures

Reynolds has developed a logic for reasoning about mutual data structures in which the pre- and postconditions are written in an intuitionistic logic enriched with a spatial form of conjuction. We investigate the approach from the point of view o f the logic BI of bunched implications of O’Hearn and Pym.