Flag(FileOn("TestAgl.res")) & Set(toto | "`Component properties'" & STAGE: FIN(INTEGER) & not(STAGE = {}) & ENTREPRISE: FIN(INTEGER) & not(ENTREPRISE = {}) & EMPLOYE: FIN(INTEGER) & not(EMPLOYE = {}) & btrue & "`Component invariant'" & stage: POW(STAGE) & entreprise: POW(ENTREPRISE) & employe: POW(EMPLOYE) & est_affecte: employe +-> entreprise & dom(est_affecte) = employe & est_signataire: employe +-> entreprise & est_signataire~: entreprise +-> employe & est_signataire: POW(est_affecte) & a_pour_responsable: stage +-> employe & dom(a_pour_responsable) = stage & est_propose: stage +-> entreprise & dom(est_propose) = stage & ran(a_pour_responsable)/\dom(est_signataire) = {} & (a_pour_responsable~;est_propose): POW(est_affecte) & "`Desaffecte_Employe preconditions in this component'" & em: dom(est_affecte) => ("`Check that the invariant (a_pour_responsable: stage --> employe) is preserved by the operation - ref 3.4'" => dom(a_pour_responsable|>>{em}) = stage))