la visibilité considérée ci -dessous ne l'est que pour la spécification, elle ne dit rien en particulier sur l'utilisation pour autre chose que des propriétés - a creuser

dans un composant, - a priori toutes les variables d'états propres au composant sont visibles à l'extérieur (que ce soit dans une assembly ou un composite) – éventuellement, prévoir une clause de masquage - si le composant est composite, les variables d'état de ses composants internes ne sont pas visibles à l'extérieur – pour rendre “visible” à l'extérieur du composite une variable d'état X:INTEGER d'un composant interne b , il faut que celle ci soit perçue comme une variable d'état du composite. Plusieurs solutions : — déclarer dans l'état du composite la variable A avec A is b.X. (l'extérieur ne verra que A : INTEGER) — déclarer dans l'état du composite la variable A: INTEGER avec A = b.X dans l'invariant (l'extérieur verra A : INTEGER puisqu'il fait partie de l'état) — ajouter une clause de visibilité/renommage b.X as A (l'extérieur ne verra que A : INTEGER)

Au sujet des propriétés :

But: l'utilisateur du composite “ a droit ” à un invariant le plus utile possible

• lorsqu'une variable est rendue visible on peut (on devrait ?) remonter toute propriété “libre” la concernant. (par libre j'entends une propriété ne comportant aucune variable masquée: si X > 10 dans b on remonte A>10 dans l'exemple précédent)
• un composite peut exprimer des propriétés utilisant les variables d'état de ses composants internes dont certaines peuvent être non visibles

Comment l'obtenir: - version brutale pas chère : masquer toute propriété qui contient une variable masquée - version brutale plus chère : intégrer les propriétés du sous composant qui portent sur la variable masquée (b.Y dans l'exemple ci dessous) F +b.Y >10 et b.Y<5 devient F > 5 … ouch

Cette version brutale plus chere devrait etre encouragée à defaut d'etre obtenue automatiquement.

Remarques additionnelles - ajouter un constructeur(service ?) utilisé ds l'assemblage pour initialiser des variables (ou plus ? ) - ajouter un support dans la verif pour les appels à des services internes : sur le canal implicite portant le nom de l'instance du composant interne