37. Adding services to an order🔗

Requirement ONE-602. Of its 4 acceptance criteria, 3 are proven and 1 is open.

rule

Rules.OneOrder.Ancillaries.addServices
  (related : Rules.OneOrder.Ancillaries.ServiceKind → Bool)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (items : List Rules.OneOrder.OrderItem) :
  Except Rules.OneOrder.Ancillaries.AddRejection Rules.OneOrder.Order
Rules.OneOrder.Ancillaries.addServices
  (related :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Bool)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (items :
    List Rules.OneOrder.OrderItem) :
  Except
    Rules.OneOrder.Ancillaries.AddRejection
    Rules.OneOrder.Order

EARS: When a seller adds services to an order, the system shall accept the request only if every flight-related ancillary in it has a live flight service for its passenger and segment, in the order or in the request.

Story: As an airline, I want a bag or a seat sold only with the flight it is for, so that no customer pays for an ancillary on a flight they do not hold.

Acceptance criteria:

ONE-602.1: If a seller adds a flight-related ancillary for a passenger on a segment, and neither the order nor the request holds a live flight service for that passenger on that segment, then the system shall refuse the request.
ONE-602.2: When a request to add services is accepted, the system shall add its order items after the existing ones and leave the existing ones as they were.
ONE-602.3: Where no service in a request is a flight-related ancillary, the system shall accept the request.
ONE-602.4: When a seller changes an order item of an order in which every live flight-related ancillary has a live flight service for its passenger and segment, the system shall keep a live flight service for the passenger and segment of every live flight-related ancillary.

Which kinds are flight related is the reading's. The last criterion asks whether the rule holds for the life of the order or only when the ancillary is bought; it is checked against the change rule for a paid change (Rules.OneOrder.Change.changeItem).

37.1. How each acceptance criterion is checked🔗

A criterion is proven when a guarantee below proves it for every input, and example only when only examples check it.

Criterion	Status	Checked by
ONE-602.1	Proven	Adding ancillaries, An ancillary without its flight is refused
ONE-602.2	Proven	Added items follow the existing ones, Adding ancillaries
ONE-602.3	Proven	Services that need no flight are added, Adding ancillaries
ONE-602.4	Open	Bag left by flight change, Ancillary needs a flight service

37.2. Guarantees🔗

37.2.1. An ancillary without its flight is refused🔗

guarantee

Rules.OneOrder.Ancillaries.add_refuses_without_flight
  (related : Rules.OneOrder.Ancillaries.ServiceKind → Bool)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (items : List Rules.OneOrder.OrderItem)
  (s : Rules.OneOrder.Service)
  (hs : s ∈ List.flatMap (fun x ↦ x.services) items)
  (hrel : Rules.OneOrder.Ancillaries.isFlightRelated related d s = true)
  (hno :
    Rules.OneOrder.Ancillaries.hasFlightFor d
        (Rules.OneOrder.Ancillaries.services o ++
          List.flatMap (fun x ↦ x.services) items)
        s =
      false) :
  ∃ e,
    Rules.OneOrder.Ancillaries.addServices related d o items =
      Except.error e
Rules.OneOrder.Ancillaries.add_refuses_without_flight
  (related :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Bool)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (items : List Rules.OneOrder.OrderItem)
  (s : Rules.OneOrder.Service)
  (hs :
    s ∈
      List.flatMap (fun x ↦ x.services)
        items)
  (hrel :
    Rules.OneOrder.Ancillaries.isFlightRelated
        related d s =
      true)
  (hno :
    Rules.OneOrder.Ancillaries.hasFlightFor
        d
        (Rules.OneOrder.Ancillaries.services
            o ++
          List.flatMap
            (fun x ↦ x.services) items)
        s =
      false) :
  ∃ e,
    Rules.OneOrder.Ancillaries.addServices
        related d o items =
      Except.error e

A request that adds a flight-related ancillary with no live flight service for its passenger and segment, in the order or in the request, is refused, under every reading of which kinds are flight related.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-602.1.

37.2.2. Added items follow the existing ones🔗

guarantee

Rules.OneOrder.Ancillaries.add_appends
  (related : Rules.OneOrder.Ancillaries.ServiceKind → Bool)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o o' : Rules.OneOrder.Order) (items : List Rules.OneOrder.OrderItem)
  (h :
    Rules.OneOrder.Ancillaries.addServices related d o items =
      Except.ok o') :
  o'.items = o.items ++ items ∧
    o'.id = o.id ∧ o'.createdAt = o.createdAt
Rules.OneOrder.Ancillaries.add_appends
  (related :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Bool)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o o' : Rules.OneOrder.Order)
  (items : List Rules.OneOrder.OrderItem)
  (h :
    Rules.OneOrder.Ancillaries.addServices
        related d o items =
      Except.ok o') :
  o'.items = o.items ++ items ∧
    o'.id = o.id ∧
      o'.createdAt = o.createdAt

An accepted request adds its order items after the existing ones, which stay as they were, and keeps the order's reference and creation instant.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-602.2.

37.2.3. Services that need no flight are added🔗

guarantee

Rules.OneOrder.Ancillaries.add_accepts_unrelated
  (related : Rules.OneOrder.Ancillaries.ServiceKind → Bool)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (items : List Rules.OneOrder.OrderItem)
  (h :
    ∀ s ∈ List.flatMap (fun x ↦ x.services) items,
      Rules.OneOrder.Ancillaries.isFlightRelated related d s = false) :
  Rules.OneOrder.Ancillaries.addServices related d o items =
    Except.ok
      { id := o.id, items := o.items ++ items,
        createdAt := o.createdAt }
Rules.OneOrder.Ancillaries.add_accepts_unrelated
  (related :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Bool)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (items : List Rules.OneOrder.OrderItem)
  (h :
    ∀
      s ∈
        List.flatMap (fun x ↦ x.services)
          items,
      Rules.OneOrder.Ancillaries.isFlightRelated
          related d s =
        false) :
  Rules.OneOrder.Ancillaries.addServices
      related d o items =
    Except.ok
      { id := o.id,
        items := o.items ++ items,
        createdAt := o.createdAt }

A request with no flight-related ancillary is accepted, under every reading.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-602.3.

37.2.4. Ancillary needs a flight service🔗

guarantee

Rules.OneOrder.Ancillaries.change_keeps_flights
  (m : Rules.OneOrder.Delivery.MoveReading)
  (related : Rules.OneOrder.Ancillaries.ServiceKind → Bool)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o o' : Rules.OneOrder.Order) (c : Rules.OneOrder.Change.ItemChange)
  (h0 : Rules.OneOrder.Ancillaries.uncovered related d o = [])
  (h : Rules.OneOrder.Change.changeItem m o c = Except.ok o') :
  Rules.OneOrder.Ancillaries.uncovered related d o' = []
Rules.OneOrder.Ancillaries.change_keeps_flights
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (related :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Bool)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o o' : Rules.OneOrder.Order)
  (c : Rules.OneOrder.Change.ItemChange)
  (h0 :
    Rules.OneOrder.Ancillaries.uncovered
        related d o =
      [])
  (h :
    Rules.OneOrder.Change.changeItem m o
        c =
      Except.ok o') :
  Rules.OneOrder.Ancillaries.uncovered
      related d o' =
    []

When every live flight-related ancillary of an order has a live flight service for its passenger and segment, a paid change to an order item keeps it so.

Open question for the business. The guide states the rule when an ancillary is bought. A change that moves a passenger's flight to another segment cancels the old flight service and leaves the bag bought for it confirmed, on a segment the passenger no longer flies. The example bagLeftByFlightChange shows it. Does the rule hold for the life of the order, and if so, what happens to the bag?

Open The proof is not complete. See the open questions chapter.

Checks acceptance criteria ONE-602.4.

37.3. Examples🔗

37.3.1. Adding ancillaries🔗

example

Rules.OneOrder.Ancillaries.addingAncillaries :
  List Rules.OneOrder.Ancillaries.AddCase
Rules.OneOrder.Ancillaries.addingAncillaries :
  List Rules.OneOrder.Ancillaries.AddCase

Given an order with one paid flight for PAX-1 on SEG-OUT, and the taxonomy reading, under which bags are flight related and insurance is not.

When the seller adds, in turn, a bag on SEG-OUT, a bag on SEG-IN and travel insurance.

Then the bag on SEG-OUT is added. The bag on SEG-IN is refused: the passenger holds no flight on that segment. The insurance is added with no flight.

What Lean computed:

Request	Refusal	Items
bag on SEG-OUT	none	2
bag on SEG-IN	no flight BAG-IN	1
travel insurance	none	2

Checks acceptance criteria ONE-602.1, ONE-602.2, ONE-602.3.

37.3.2. Bag left by flight change🔗

example

Rules.OneOrder.Ancillaries.bagLeftByFlightChange :
  Except Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Ancillaries.CoverAfterChange
Rules.OneOrder.Ancillaries.bagLeftByFlightChange :
  Except
    Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Ancillaries.CoverAfterChange

Given an order with a paid flight for PAX-1 on SEG-OUT and a paid bag for the same passenger and segment in its own item, under the taxonomy reading.

When the seller makes a paid change that moves PAX-1 to a flight on SEG-NEW.

Then the old flight is cancelled and the bag stays confirmed on SEG-OUT, which the passenger no longer flies. Before the change every bag had its flight; afterwards the bag has none.

What Lean computed:

Accepted. The result:

Ancillaries without flight before: none
Old flight: cancelled
Bag: confirmed
Bag segment: SEG-OUT
Ancillaries without flight after: BAG-OUT

Checks acceptance criteria ONE-602.4.

37.4. Open question🔗

The guarantee Ancillary needs a flight service is open: the example Bag left by flight change shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.