Modularity and Resource Separation

Modularity is a key concept which programmers wield in their struggle againstthe complexity of software systems. When a program is divided into conceptually distinct modules or components, each of which uses separate internal resources (such as storage),the effort required for understanding the program is decomposed into circumscribed, hopefully manageable, parts. The purpose of this project is to bring separation logic to bear on modularity.The separating conjunction connective will be used to give a precise, theoretical expression that correspondsto the existing pre-formal, intuitive link between resource separation and modularity.We will develop semantic models that describe when a piece of state used by a module is held separate from the clients that use it. Theories of refinement and parametricity will be studied. The former will begin to address one of the common criticisms of separation logic,that verifications take place on a fixed (low) level of abstraction. The latter will give us methods for showing equivalence of imperative modules and for understanding information hiding for imperative resources. We will also investigate methods for proof and static checking and analysis for imperative modules. This project contribute considerably to the problems of scalable reasoning about programs and protection of resources from outside tampering, in the presence of practical programming features such as pointers thathave previously been seen as barriers to technically precise accounts of modularity.