Formale Repräsentation der Komponentenspezifikation AirlineSystemSpec FRep(AirlineSystemSpec) = ( , Invs, OpSpecs) wobei Invs aus den expliziten Invarianten Invs^{e} und den folgenden impliziten Invarianten Invs^{i} besteht. Implizite Invarianten Invs^{i}: =================================================== wegen Airline 1-----> Person, Fall 2.2 angepasst an multB > 1 context AirlineSystem inv invOneAirlineForPerson: Person.allInstances() -> forAll( p | Airline.allInstances() -> one( a | a.employees -> includes(p) ) ) ==================================================== wegen Person 2..*-----> Flight Fall 2.4 mit 2..* statt 1..* context AirlineSystem inv invAtleastTwo: Flight.allInstances() -> forAll( f | Person.allInstances() -> select( p | p.flights -> includes(f) ) -> size() >= 2 ) ==================================================== wegen Airline 1----- Flight Fall 1.2 context Flight inv invOneAirlineForFlight: airline <> null ==================================================== wegen Airline ----- Flight (Bidirektionalität) Mischform von Fall 3.2 und Fall 3.4 context AirlineSystem inv invBidirect: Flight.allInstances() -> forAll( f | f.airline.flights -> includes(f) ) and Airline.allInstances() -> forAll( a | a.flights -> forAll( f | f<>null implies f.airline = a ) ) ==================================================== wegen Person {abstract} context AirlineSystem inv invPersonAbstract: Person.allInstances() -> select( p | p.oclIsTypeOf(Person) ) -> isEmpty()