Refinement and Separation Contexts

A separation context is a client program which does not dereference internals of a module with which it interacts. We use certain "precise" relations to unambiguously describe the storage of a module and prove that separation contexts preserve such relations. We also show that a simulation theorem holds for separation contexts, while this is not the case for arbitrary client programs.

• Type: Conference
• Year: 2004
• Where: FSTTCS
• Authors: Ivana Mijajlovic, Noah Torp-Smith, Peter W. O'Hearn
• Keywords: Arbitrary Client Programs, Client Programs, FSTTCS 2004, Separation Contexts, Software Engineering