In separation logic, Hoare triples have a slightly different meaning than in Hoare logic. The triple formula_52 asserts that if the program formula_53 executes from an initial state satisfying the precondition formula_12 then the program will "not go wrong" (e.g., have undefined behaviour), and if it terminates, then the final state will satisfy the postcondition formula_14. In essence, during its execution, formula_53 may access only memory locations whose existence is asserted in the precondition or that have been allocated by formula_53 itself.