With Sylvain Boulmé :

One of the major aspects of the B method is its notion of component (abstract machine, 
refinement and implementation) which can be proved and developed in an independent 
way. Invariant can be stated relatively to the variables and operations  set defined in  a 
given component. Proof obligations are made at the level of component definition and the 
compositionality principle ensures invariant preservation in any admissible B 
compositions. Compositionality is based on a set of rules which control how components 
are used and combined, resulting in that in  no further proof obligations. In this way 
invariant composition is a transparent process for developers as soon as they respect B restrictions.

On the other hand the Spec# approach is based on the dynamic notion of "ownership"
which characterizes which object instance can constrain, through an invariant, others 
object instances. The Spec# approach is based on a set of meta-invariants which
describe in which point invariants are guaranted, depending on the ownership relation.
This approach is a very flexible one but the counterpart is that developers must master
invariant compositionality through meta-invariants and meta-instructions allowing them to
locally invalidate or validate invariants. A solution is to use meta-schemas (as design 
patterns), which are pre-labelled by information about invariant validity, corresponding to 
classical architecture forms. For instance the B restrictions can be seen as meta-schemas 
which ensure, by construct, invariant preservation in all points outside the concerned 
operations.

The aim of the talk is to show how the actual architectural restrictions of the B method
can be interpreted as a particular case of Spec# ownership relation and to propose some 
extensions to make these restrictions less strict,  without too complicated overheads for 
developers. Finally we study how invariant composition and refinement can interact.