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
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