Komponentenspezifikation AirlineSystemSpec = ( , Invs^{e}, OpSpecs) ================================================================ Explizite Invarianten (Invs^{e}): (a) context Person inv invSalary: salary > 0 and salary <= 20000 (b) 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) )) ) ) (c) 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) ) ) (d) context Airline inv invPartners: partners -> excludes(self) (e) context AirlineSystem inv invPartnersViceVersa: Airline.allInstances() -> forAll( a | a.partners -> forAll( pa | pa.partners -> includes(a) ) ) ================================================================ Operationsspezifikationen (OpSpecs): //Airline Operationen context Airline::Airline(n: String) pre: n <> "" post: name = n and employees -> isEmpty() and flights -> isEmpty() and partners -> isEmpty() context Airline::createPilot(n: String, s: Real): Pilot pre: n <> "" and s > 0 and //wegen post und (a) (Vertraeglichkeit der Nachbedingung mit den Invarianten) s <= 20000 post: result.oclIsNew() and result.name = n and result.salary = s and result.flights -> isEmpty() and 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: no > 0 and p<>null and s<>null and //wegen (*) und (b) (employees -> includes(p) or partners -> exists( pa | pa.employees -> includes(p))) and //wegen (**) und (b) (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 p.flights -> excludes(f) and //wegen post und (b) flights -> includes(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.partners -> excludes(self) and //wegen post und (d) a<>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) //Flight-Operationen context Flight::Flight(no: Integer, a: Airline) pre: no > 0 and 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 //Person-Operationen 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 //wegen (*) und (a) salary + i <= 20000 post: salary <= salary@pre + i and (*) salary > salary@pre //Pilot-Operationen context Pilot::Pilot(n: String, s: Real) pre: n <> "" and s > 0 and //wegen post und (a) s <= 20000 post: name = n and salary = s and flights -> isEmpty() context Pilot::increase(i: Real) pre: i > 0 and //wegen post und (a) salary + i <= 20000 post: salary = salary@pre + i //Steward-Operationen context Steward::Steward(n: String, s: Real) "analog zu Pilot" context Steward::increase(i: Real) pre: i > 0 and //wegen post und (a) salary + i/2 <= 20000 post: salary = salary@pre + i/2