Separation Logic: {{A}} Logic for Shared Mutable Data Structures