Proving the absence of Cross Bindings

In this section we show how we can prove one of the properties that is expected to hold in any GCM application. GCM inherits a lot of its features from Fractal, and as such many properties expected to hold in Fractal, are also expected to hold in GCM. From the Fractal specification, we know that there are 3 types of bindings: Normal, Export and Import. It is stated in the Fractal specification that if a binding meets the constraint of being of Normal, Export or Import type, then it cannot cross any component boundary except through its interfaces. In the following, we demonstrate how this can be proved within our framework.

Preliminary Definitions - Setting Up the Scene!

First of all, we to define what it means to be a cross binding. Since we have 3 types of bindings, Normal, Export and Import, we gonna have 3 types of cross bindings. As such, we need to define each of them w.r.t. our framework.

The 3 above definitions cross_normal, cross_export and cross_import define what it means to be a cross binding of type Normal, Export and Import, respectively. Essentially, they all state that the "second part" of the binding (idC2 IdI2, for id of second component and id of second interface, resp.), is located at a different level in the component hierarchy. Since we use idents to identify components and interfaces, and since they need not to be unique among different levels of the hierarchy, we need to explicitly state that there exists no component and/or interface with such ident. From this, we can proceed to the remaining few definitions that basically just place the above ones in the context of our hierarchical component framework.

Cross Bindings Cannot Occur? Proof? Sure thing!

Before proceeding proving the property we want, we shall first prove a lemma that states that if a binding is valid, then it cannot be crossing. This lemma will serve as an auxiliary to prove our main theorem.

The proof of binding_cannot_be_crossing_if_valid gives us that a binding cannot be valid and crossing for the same state. The argument of the proof is essentially a case analysis on the binding type, where we show a contradiction for all of the 3 constructors. The proof above, although a little bit long, should pose no trouble to the reader. Our definition of cross_bindings is defined in a way that makes this proof easy, as it requires to explicitly negate the presence of a component and/or interface that would match the specified idents in the "second part" of the cross_binding. This is a direct implication of the data structure used to defined our hierarchical component framework. As usual in Coq developments relying on inductive definitions, choosing adequates data structures may considerably ease the burden of theorem proving. We shall now proceed to one last definition before moving to the main proof. We define a predicate system_binding that states whether a binding belongs to a state.

The key to the proof of our main theorem cross_binding_cannot_happen lies in the argument of our previously proved lemma binding_cannot_be_crossing_if_valid. The idea is to show that any binding present in the state must be a valid_component_binding - this follows from the fact that the state is well_formed. Then, since we know from binding_cannot_be_crossing_if_valid that a binding cannot be a valid_component_binding and a valid_cross_binding at the same time, we can conclude the proof.