Formale Repräsentation der Komponentenspezifikation AirlineSystemSpec

FRep(AirlineSystemSpec) = (<AirlineSystem, \Sigma_{Delta}>, Invs, OpSpecs)

wobei Invs aus den expliziten Invarianten Invs^{e}
und den folgenden impliziten Invarianten Invs^{i} besteht.

Implizite Invarianten:

context AirlineSystem
  inv  invPersonAbstract:
       Person.allInstances() =
       Pilot.allInstances() -> union(Steward.allInstances())

context AirlineSystem
  inv  invOneAirline:
       Person.allInstances() -> forAll( p |
         Airline.allInstances() -> one( a |
	   a.employees -> includes(p)))

context AirlineSystem
  inv  invAtleastTwo:
       Flight.allInstances() -> forAll( f |
         Person.allInstances() -> select( p |
	   p.flights -> includes(f)) -> size() >= 2)

context Flight
  inv: airline <> null

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