% Project: ECONET 
% Document: Prague07 Workshop Report
% Last writer: Andre Pascal 
% creation: 14/09/07 
% modification PA 02/10/07 
% *********************************** 
%\section{Metamodel Abstraction Subproject}
%\label{metamodel}

\textit{Writer: Dan Chiorean} 
%\\

%NB: \textit{currently in romanian, put in a latex format by pascal, it will be translated soon}.

\subsection{Objectives and Goals}
\subsection{Participants}
\subsection{Means}
\subsection{Tasks and Schedule}

??

\subsection{Using assertions in modeling - an evaluation time view}

Using assertions in modeling is incomplete if this is restrained just to better understand the problem and to emphasize the conditions that have to be accomplished by the clients and the provider of a functionality.  The true benefits can be obtained only if assertions are used at runtime, assisting the user in preventing software runtime crashes or obtaining inaccurate results.  Our interest is not limited to validation.  In case of constraint violation, we are interested in identifying rationales and even more, in fixing bugs and errors.  The price that needs to be paid for obtaining the maximum benefits from using assertions in modeling is to take into account the moment when constraints are evaluated.  The main target of this paper is to highlight the manner in which the moment when assertions are evaluated influences their specification.
 
\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/metaCCM.eps,width=15cm}}
\caption{A part of the CoreComponent Metamodel}%[metaCCM]
\label{metaCCM}
\end{figure}

%Figure 1 - 

In order to support an easier understanding of our statements, we will consider the CoreComponents metamodel - a simple model grouping the common features of most component-oriented modeling languages \cite{dsrg:BuHnSOFA202006}.  Moreover, in Figure 1, only the elements referred in assertions are represented.

Model validation (model checking) can be regarded from two perspectives (views): static checking and dynamic checking.  As we will see in the following, these views influence assertions' specification.

\subsection{Static checking - The constraints aid in correcting and validating a previously constructed model}

Models are metamodel instances - our objective is to check if the analyzed models comply with all the constraints associated to different metamodel elements.  The problem is entirely similar with that of an UML model validated against WFR specified at the UML metamodel level.  In this case, constraints are specified by means of invariants.

As mentioned in \cite{rat:moors}, during its construction, the model is incomplete and sometimes it is incorrect against the constraints associated to the modeling language.  Therefore, before doing model transformation, it is important to check model correctness and completeness (model compilability).

In case of the \texttt{CoreComponents} metamodel, the {\sc xor} constraint between the unidirectional associations from \texttt{SubcomponentInstance} toward \texttt{Frame} and \texttt{Architecture} (graphically specified in Figure \ref{metaCCM}), can be expressed by means of the following invariant:

\begin{verbatim}
(1) context SubcomponentInstance
     inv FrameOrArchitectureAssoc:
       self.instantiateArchitecture.isUndefined xor self.instantiateFrame.isUndefined
\end{verbatim}

If the above invariant's value is \texttt{false}, evaluating both its {\sc xor}  sub-expressions supports the developer in identifying error's rationale, enabling, this way, error fixing.

The constraint concerning the name uniqueness of required interfaces associated to an instance  of the \texttt{Frame} metaclass, specified by means of the following invariant:

\begin{verbatim}
(2) context Frame
     inv requiredInterfacesName:
       self.requiredInterface.name->isUnique(n | n)
\end{verbatim}

does not support enough the user in identifying interfaces that caused this invariant's violation.  This is because in case of many interfaces, a careful study of their names is time consuming, tedious and error prone.
 
\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/sofaDB.eps,width=8cm}}
\caption{Components with provided and required Interfaces}%[sofaDB]
\label{sofaDB}
\end{figure}
%Figure 2 

A more appropriate specification, aiding the user in identifying interfaces with the same name is:

\begin{verbatim}
(3) context Frame
     inv requiredInterfacesName:
       let ri = self.requiredInterface in
       (ri->reject(e | ri.name->count(e.name)=1))->isEmpty
\end{verbatim}

In case of an invariant violation, simply evaluating the collection of interfaces having identical names helps the user in navigating the above mentioned interfaces and in model updating (correction), in order to comply with this invariant (see Figure \ref{sofaOcle}).

\begin{figure}[ht]
\centerline{\epsfig{figure=\repFIGURES/sofaOcle.eps,width=16cm}}
\caption{Components with provided and required Interfaces}%[sofaOcle]
\label{sofaOcle}
\end{figure}
%Figure 3 

If the uniqueness condition concerns both required and provided interfaces, the specification could be:

\begin{verbatim}
(4) context Frame
     inv uniqueInterfacesName:
       let i = self.requiredInterface->union(self.providedInterface) in
       (ri->reject(e | ri.name->count(e.name)=1))->isEmpty
\end{verbatim}

Comparing the specifications presented in (3) and (4) with the specification presented in (2), we can notice that the price paid for an easier identification of interfaces violating the \texttt{Frame} invariant \texttt{requiredInterfacesName} (Figure \ref{sofaOcle}) is a more detailed OCL specification.

In case of constraints restraining the type of elements that can be associated as \texttt{Frame} annotations, we will adopt a solution similar to the previous one:

\begin{verbatim}
(5) context Frame
     inv annotations_Type:
       self.annotation->select(e | not e.oclIsTypeOf(TopLevel))->isEmpty
\end{verbatim}

Like for specifications presented in (3) and (4), the objective is not restricted to catch invariant violation.  We are interested in identifying the rationale of this failure.  Evaluating the collection returned by the select operation (5) supports users in identifying the annotations violating this constraint.

\subsection{Dynamic checking - The constraints aid in preserving the model valid after each operation}

This situation is similar to that of an object-oriented application, in which objects are created, destroyed or change their state.  The universe of these objects has to be permanently valid.  Therefore, we have to take appropriate decisions, enabling us to keep the system in a valid state after each call of a constructor or of a modifier.  The strategy adopted will comply with the philosophy "better prevent than cure", therefore, the constraints will be specified mainly by means of pre and postconditions.

As in the static checking case, we will first analyze the constraint between the two unidirectional associations starting from the \texttt{SubcomponentInstance} class toward \texttt{Frame} and \texttt{Architecture}.  The  {\sc xor} constraint (graphically specified on the class diagram) states that starting from \texttt{SubcomponentInstance} we will always have a single association, either toward the \texttt{Frame} class, or toward the \texttt{Architecture} class.

According to the "design by contract" principle \cite{meyer-book}, the invariant specified for the \texttt{SubcomponentInstance} class has to be satisfied by all its instances during their entire life, excepting the time when modifiers are applied on those instances.  A first consequence is that \texttt{SubcomponentInstance} objects must be created always using explicit constructors.  In case of a single explicit constructor, among its parameters we should have a valid reference toward one of the \texttt{Frame} or \texttt{Architecture} classes and only one.  Therefore, the other reference has to be null (\texttt{undefined}).  An alternative for the invariant will be:

\begin{verbatim}
(6) context SubcomponentInstance::SubcomponentInstance(a:Architecture, 
                                          f:Frame):SubcomponentInstance
     pre subcomponentInstance_connection:
       (a.isUndefined and f.oclIsTypeOf(Frame)) or 
       (f.isUndefined and a.oclIsTypeOf(Architecture))
     post subcomponentInstance_connection_:
       (result.instantiateFrame = f) and (result.instantiateArchitecture = a)
\end{verbatim}

The OOP philosophy requires the methods \texttt{setInstantiateFrame(f:Frame)} and \texttt{setInstantiateArchitecture(a:Architecture)} to update only the value of the \texttt{associationEnd} transmitted as a parameter.  Therefore, in case of these modifiers, the pre and postconditions could be:

\begin{verbatim}
(7) context SubcomponentInstance::setInstantiateFrame(f:Frame) 
     pre instantiate_Frame:
       self.instantiateArchitecture.isUndefined and f.oclIsTypeOf(Frame)
     post instantiate_Frame:
       self.instantiateFrame = f
\end{verbatim}

\begin{verbatim}
(8) context SubcomponentInstance::setInstantiateArchitecture (a: Architecture) 
     pre instantiate_Architecture:
       self.instantiateFrame.isUndefined and a.oclIsTypeOf(Architecture)
     post instantiate_Architecture_:
       self.instantiate Architecture = a
\end{verbatim}

If the requirements explicitly mention that in case of a \texttt{SubcomponentInstance} object it is possible to remove its association toward a \texttt{Frame} instance and to add a new association toward an \texttt{Architecture} instance (to switch from a \texttt{Frame} to an \texttt{Architecture}) or vice versa, the operation supporting this requirement must comply with a precondition similar to that above specified for the explicit constructor.  In the body of that method, an appropriate \texttt{setInstantiate} method will be called just after setting the other possible reference to null.

Regarding the constraints ensuring the uniqueness of the names of \texttt{requiredInterfaces} attached to a \texttt{Frame}, we will take into account the fact that this constraint can be broken only when a new interface is added. Therefore, the assertions attached to the operation \texttt{addRequiredInterface(i:Interface)} would be:

\begin{verbatim}
(9) context Frame::addRequiredInterface(i:Interface)
     pre uniqueName:
       i.name.size > 0 and self.requiredInterface.name->excludes(i.name)
     post uniqueName_:
       self.requiredInterface->size = self.requiredInterface@pre->size + 1 and 
       self.requiredInterface.name->includes(i.name)
\end{verbatim}

If changing the interface name after attaching the interface to a Frame is required, then, an appropriate precondition has to be specified for the method \texttt{Interface::setName(n: String)}.  Also, if explicit constructors initializing the value of the requiredInterface role (toward \texttt{Interface} objects) were specified for the class \texttt{Frame}, then, appropriate preconditions have to be specified for those above mentioned constructors.

The last constraint concerns the type of instances that can be attached to a Frame as annotations.  In this case, the assertion will also be specified by means of a precondition.

\begin{verbatim}
(10) context Frame::addAnnotation(a:Annotation)
      pre param_s_type:
        a.oclIsKindOf(TopLevel)
\end{verbatim}

\subsection{Conclusion}

When specifying assertions, the evaluation time must be taken into account.  In case of static evaluation, the assertions are mainly specified by means of invariants.  The invariant specification has to help designers in identifying the rationales of invariant failure.  The price to be paid is a detailed OCL specification.  In case of dynamic evaluation, the assertions are mainly specified by using pre and postconditions.  At runtime, assertions specified in OCL are translated in the target programming language.  Therefore managing assertions failure must consider both the support of the programming language and the functionalities offered by the IDE used.


\endinput

