In this section we prove that our operation language complies with the GCM Specification. We discuss all the auxiliary lemmas that allow us to prove our main theorem stating that provided that our semantic rules are respected, any produced GCM Architecture will indeed meet the GCM Specification.

Meeting the Specification

In the previous sections we mechanized a semantics for an operation language permitting the building of GCM Architectures. Each language constructor was rigorously defined. Moreover, a set of auxiliary lemmas was proved in order to ease our subsequent development. This section shows that our operation language indeed respects the GCM specification.

Making Components

Very well, after the above preliminary machinery we can now start reasoning on how to attack this proof. First of let us start by showing that the produced component hierarchy l2 originates from adding our component _(Component id t p cl lc li lb)_ to l. This is achieved as follows:

The above as quite easy, let us now prove that the component hierarchy produced by adding a component is always well formed. In this case, we will only need to apply our previously proved lemma well_formed_adding_component and then do some minor footwork.

As of now, all the above was pretty much just to "setup the stage", that is, preparing our context for actually proving our lemma. Indeed, we are now in position to prove that after adding a well formed component, in a well formed stated, we will end up in a well formed state.

Removing Components

Making Interfaces

As in the lemma valid_mk_comp, we do the above footwork to ease our proof below. Now we can focus on the most relevants aspects, namely the fact that adding a component in the hierarchy always yields a well formed hierarchy. This is achieved by applying a previously proved lemma, and doing some minor steps in order to make our context satisfy the necessary hypotheses.

As before, we also make this simple assertion just to ease the proof development.

As a last auxiliary step, we ensure that adding an interface does not affect the well formedness of bindings.

and finnaly, le coup the grace!

Making Bindings

As in the lemma valid_mk_comp, we do the above footwork to ease our proof below. Now we can focus on the most relevants aspects, namely the fact that adding a binding in the hierarchy always yields a well formed hierarchy. This is achieved by applying a previously proved lemma, and doing some minor steps in order to make our context satisfy the necessary hypotheses.

And now we can prove this lemma! You'll notice that this one requires a little bit more tweaking than its "brothers" above. This should come as no surprise, since it envolves linking components by means of their interfaces.

Note that this assertion is only true if path <> nil. Otherwise the binding is inserted at the Root level.

As usual, we need to ensure that the bindings remain well formed after adding a binding in the hierarchy.

And now, finally, the last steps for victory!

Removing Bindings

In this section we prove that our operation language complies with the GCM Specification. We discuss all the auxiliary lemmas that allow us to prove our main theorem stating that provided that our semantic rules are respected, any produced GCM Architecture will indeed meet the GCM Specification.