Komponentenspezifikation AirlineSystemSpec


Explizite Invarianten:

context Person
  inv: salary >=0 and salary <= 20000

context AirlineSystem
  inv  invEmployeeFlight:
       Person.allInstances() -> forAll( p |
         p.flights -> forAll( f |
           (f.airline.employees -> includes(p)) or
	   (f.airline.partners -> exists( pa |
             pa.employees -> includes(p)))))

context AirlineSystem
  inv  invExistsPilotSteward:
       Flight.allInstances() -> forAll( f |
         Pilot.allInstances() -> exists( p |
           p.flights -> includes(f)) and
         Steward.allInstances() -> exists( s |
           s.flights -> includes(f)))

context Airline
  inv: partners -> excludes(self)

context AirlineSystem
  inv  invPartners:
       Airline.allInstances() -> forAll( a |
         a.partners -> forAll( pa |
	   pa.partners -> includes(a)))

Implizite Invarianten:

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

context Flight
  inv: airline <> null

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



Operationsspezifikationen:

context Airline::Airline(n: String)
  post: name = n

context Airline::createPilot(n: String, s: Real): Pilot
   pre: s >= 0 and s <= 20000
  post: result.oclIsNew() and
        result.name = n and result.salary = s and result.flights -> isEmpty()
	employees = employees@pre -> including(result)

context Airline::createSteward(n: String, s: Real): Steward
   "analog"

context Airline::createFlight(no: Integer, p: Pilot, s: Steward): Flight
   pre: p<>null and s<>null and
        (employees -> includes(p) or
	 partners -> exists( pa | pa.employees -> includes(p))) and
        (employees -> includes(s) or
	 partners -> exists( pa | pa.employees -> includes(s))) and
  post: result.oclIsNew() and
        result.number = no and result.airline = self and
	flights = flights@pre -> including(result) and
        p.flights = p.flights@pre -> including(result) and
        s.flights = s.flights@pre -> including(result)

context Airline::deploy(p: Person, f: Flight)
   pre: p<>null and f<>null and
        flights -> includes(f) and
	p.flights -> excludes(f) and
        (employees -> includes(p) or
	 partners -> exists( pa | pa.employees -> includes(p)))
  post: p.flights = p.flights@pre -> including(f)

context Airline::cooperate(a: Airline)
   pre: a<>null and self.partners -> excludes(a) and
        a<>self and a.partners -> excludes(self)
  post: self.partners = self.partners@pre -> including(a) and
        a.partners = a.partners@pre -> including(self)

context Airline::hire(p: Person)
   pre: p<>null and employees -> excludes(p)
  post: employees = employees@pre -> including(p)

context Airline::addFlight(f: Flight)
   pre: f<>null and flights -> excludes(f)
  post: flights = flights@pre -> including(f)




context Flight::Flight(no: Integer, a: Airline)
   pre: a<>null
  post: number = no and airline = a

context Flight::business(): Real
  post: 3*basicPrice <= result and result <= 5*basicPrice

context Flight::economy(): Real
  post: result = 1.5*basicPrice




context Person::deploy(f: Flight)
   pre: f<>null and flights -> excludes(f)
  post: flights = flights@pre -> including(f)

context Person::increase(i: Real)
   pre: i >= 0 and salary + i <= 20000
  post: salary <= salary@pre + i



context Pilot::Pilot(n: String, s: Real)
   pre: s >= 0 and s <= 20000
  post: name = n and salary = s and flights -> isEmpty()

context Pilot::increase(i: Real)
   pre: i >= 0 and salary + i <= 20000
  post: salary = salary@pre + i



context Steward::Steward(n: String, s: Real) "analog zu Pilot"

context Steward::increase(i: Real)
   pre: i >= 0 and salary + i/2 <= 20000
  post: salary = salary@pre + i/2