15. Cancelling an order🔗

Requirement ONE-203. Of its 5 acceptance criteria, 3 are proven and 2 are open.

rule

Rules.OneOrder.Change.requestCancellation
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Change.ExcessPenalty) (o : Rules.OneOrder.Order)
  (payments : List Rules.OfferOrder.Payment)
  (t : Rules.OneOrder.Change.CancelTerms) :
  Rules.OneOrder.Change.CancelOutcome
Rules.OneOrder.Change.requestCancellation
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.Change.ExcessPenalty)
  (o : Rules.OneOrder.Order)
  (payments :
    List Rules.OfferOrder.Payment)
  (t :
    Rules.OneOrder.Change.CancelTerms) :
  Rules.OneOrder.Change.CancelOutcome

EARS: When a seller asks to cancel an order, the system shall cancel it at once if no payment has been received for it, and otherwise only through a cancellation offer.

Story: As a seller, I want an unpaid order cancelled at once and a paid order cancelled through an offer, so that every cancellation that returns money is priced first.

Acceptance criteria:

ONE-203.1: When a seller asks to cancel an order for which no payment has been received, the system shall cancel and remove at once every service of the order that the delivery status table lets be removed.
ONE-203.2: When an order is cancelled at once, the system shall mark each of its items cancelled and the order closed.
ONE-203.3: If a seller asks to cancel an order for which any payment has been received, then the system shall cancel it only through a cancellation offer.
ONE-203.4: When an order with payments is cancelled through an offer, the system shall not make the amount due by the airline larger than the payments received for the order.
ONE-203.5: When an order with payments is cancelled through an offer, the system shall price the cancellation from the order items that still hold a live service.

The payments received are the pilot model's payments for the order (Rules.OfferOrder.totalPaid). The offer is priced with priceDifferential from the items that still hold a live service (pricedItems). An item whose services a change transferred or cancelled stays in the order with its price, and this keeps it from being returned a second time. A service that the delivery status table does not let be removed, such as one still REQUESTED, one UNABLE TO DELIVER or one already DELIVERED, stays as it was (Delivery.endWith); while it is live, its item is priced.

15.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-203.1	Proven	Unpaid orders are cancelled at once, Unpaid cancellation while requested, Unpaid cancellation
ONE-203.2	Open	Orders cancelled at once are closed, Unpaid cancellation while requested, Unpaid cancellation
ONE-203.3	Proven	Paid cancellation, Paid or partly paid orders need an offer, Partly paid cancellation
ONE-203.4	Open	Cancellation offers stay within payments, Partly paid cancellation
ONE-203.5	Proven	Cancel after change, Offer priced from live items

15.2. Guarantees🔗

15.2.1. Unpaid orders are cancelled at once🔗

guarantee

Rules.OneOrder.Change.unpaid_cancelled_at_once
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Change.ExcessPenalty) (o : Rules.OneOrder.Order)
  (payments : List Rules.OfferOrder.Payment)
  (t : Rules.OneOrder.Change.CancelTerms)
  (h : Rules.OfferOrder.totalPaid payments o.id = 0) :
  ∃ o',
    Rules.OneOrder.Change.requestCancellation m r o payments t =
        Rules.OneOrder.Change.CancelOutcome.cancelled o' ∧
      List.map (fun x ↦ x.id) o'.items =
          List.map (fun x ↦ x.id) o.items ∧
        ∀ i ∈ o.items,
          ∀ s ∈ i.services,
            (Rules.OneOrder.Delivery.nextDelivery m
                    Rules.OneOrder.Delivery.DeliveryEvent.remove
                    s).isSome =
                true →
              ∃ i' ∈ o'.items,
                i'.id = i.id ∧
                  { id := s.id, passenger := s.passenger,
                      segment := s.segment,
                      status := Rules.OneOrder.ServiceStatus.cancelled,
                      delivery :=
                        Rules.OneOrder.DeliveryStatus.removed } ∈
                    i'.services
Rules.OneOrder.Change.unpaid_cancelled_at_once
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.Change.ExcessPenalty)
  (o : Rules.OneOrder.Order)
  (payments :
    List Rules.OfferOrder.Payment)
  (t : Rules.OneOrder.Change.CancelTerms)
  (h :
    Rules.OfferOrder.totalPaid payments
        o.id =
      0) :
  ∃ o',
    Rules.OneOrder.Change.requestCancellation
          m r o payments t =
        Rules.OneOrder.Change.CancelOutcome.cancelled
          o' ∧
      List.map (fun x ↦ x.id) o'.items =
          List.map (fun x ↦ x.id)
            o.items ∧
        ∀ i ∈ o.items,
          ∀ s ∈ i.services,
            (Rules.OneOrder.Delivery.nextDelivery
                    m
                    Rules.OneOrder.Delivery.DeliveryEvent.remove
                    s).isSome =
                true →
              ∃ i' ∈ o'.items,
                i'.id = i.id ∧
                  { id := s.id,
                      passenger :=
                        s.passenger,
                      segment :=
                        s.segment,
                      status :=
                        Rules.OneOrder.ServiceStatus.cancelled,
                      delivery :=
                        Rules.OneOrder.DeliveryStatus.removed } ∈
                    i'.services

An order with no payment is cancelled at once and keeps its items: every service that the delivery status table lets be removed is cancelled and removed, under every reading of the sources.

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

Checks acceptance criteria ONE-203.1.

15.2.2. Orders cancelled at once are closed🔗

guarantee

Rules.OneOrder.Change.cancelled_at_once_closed
  (m : Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading)
  (r : Rules.OneOrder.Change.ExcessPenalty)
  (o o' : Rules.OneOrder.Order)
  (payments : List Rules.OfferOrder.Payment)
  (t : Rules.OneOrder.Change.CancelTerms)
  (h :
    Rules.OneOrder.Change.requestCancellation m r o payments t =
      Rules.OneOrder.Change.CancelOutcome.cancelled o') :
  (∀ i ∈ o'.items,
      Rules.OneOrder.itemStatuses v i =
        [Rules.OneOrder.ItemStatus.cancelled]) ∧
    Rules.OneOrder.orderStatuses v o' =
      [Rules.OneOrder.OrderStatus.closed]
Rules.OneOrder.Change.cancelled_at_once_closed
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading)
  (r :
    Rules.OneOrder.Change.ExcessPenalty)
  (o o' : Rules.OneOrder.Order)
  (payments :
    List Rules.OfferOrder.Payment)
  (t : Rules.OneOrder.Change.CancelTerms)
  (h :
    Rules.OneOrder.Change.requestCancellation
        m r o payments t =
      Rules.OneOrder.Change.CancelOutcome.cancelled
        o') :
  (∀ i ∈ o'.items,
      Rules.OneOrder.itemStatuses v i =
        [Rules.OneOrder.ItemStatus.cancelled]) ∧
    Rules.OneOrder.orderStatuses v o' =
      [Rules.OneOrder.OrderStatus.closed]

An order cancelled at once has every item cancelled and is closed, under every reading of the guide.

Open question for the business. A cancellation removes each service through the delivery status table, and the table has no move to REMOVED from REQUESTED or from UNABLE TO DELIVER, under any reading. A service the airline has not yet confirmed therefore stays REQUESTED, and its item is not cancelled. The example unpaidCancellationWhileRequested shows it. A service UNABLE TO DELIVER, such as one on a flight the airline cancelled, stays too, so cancelling that order never closes it. Under the readings that refuse to cancel a service IN PROGRESS, or that allow delivery before payment, a service IN PROGRESS or already DELIVERED stays as well. Can a seller cancel a service the airline is still deciding on, or one the airline cannot deliver, and what delivery status does it take?

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

Checks acceptance criteria ONE-203.2.

15.2.3. Paid or partly paid orders need an offer🔗

guarantee

Rules.OneOrder.Change.paid_needs_offer
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Change.ExcessPenalty) (o : Rules.OneOrder.Order)
  (payments : List Rules.OfferOrder.Payment)
  (t : Rules.OneOrder.Change.CancelTerms)
  (h : 0 < Rules.OfferOrder.totalPaid payments o.id) :
  (∃ d,
      Rules.OneOrder.Change.requestCancellation m r o payments t =
        Rules.OneOrder.Change.CancelOutcome.offer d) ∨
    ∃ e,
      Rules.OneOrder.Change.requestCancellation m r o payments t =
        Rules.OneOrder.Change.CancelOutcome.rejected e
Rules.OneOrder.Change.paid_needs_offer
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.Change.ExcessPenalty)
  (o : Rules.OneOrder.Order)
  (payments :
    List Rules.OfferOrder.Payment)
  (t : Rules.OneOrder.Change.CancelTerms)
  (h :
    0 <
      Rules.OfferOrder.totalPaid payments
        o.id) :
  (∃ d,
      Rules.OneOrder.Change.requestCancellation
          m r o payments t =
        Rules.OneOrder.Change.CancelOutcome.offer
          d) ∨
    ∃ e,
      Rules.OneOrder.Change.requestCancellation
          m r o payments t =
        Rules.OneOrder.Change.CancelOutcome.rejected
          e

An order with any payment is never cancelled at once. The request leads to a cancellation offer, or to a rejection when the cancellation cannot be priced.

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

Checks acceptance criteria ONE-203.3.

15.2.4. Cancellation offers stay within payments🔗

guarantee

Rules.OneOrder.Change.offer_within_payments
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Change.ExcessPenalty) (o : Rules.OneOrder.Order)
  (payments : List Rules.OfferOrder.Payment)
  (t : Rules.OneOrder.Change.CancelTerms)
  (d : Rules.OneOrder.Change.PriceDifferential)
  (h :
    Rules.OneOrder.Change.requestCancellation m r o payments t =
      Rules.OneOrder.Change.CancelOutcome.offer d) :
  d.dueByAirline.amount ≤ Rules.OfferOrder.totalPaid payments o.id
Rules.OneOrder.Change.offer_within_payments
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.Change.ExcessPenalty)
  (o : Rules.OneOrder.Order)
  (payments :
    List Rules.OfferOrder.Payment)
  (t : Rules.OneOrder.Change.CancelTerms)
  (d :
    Rules.OneOrder.Change.PriceDifferential)
  (h :
    Rules.OneOrder.Change.requestCancellation
        m r o payments t =
      Rules.OneOrder.Change.CancelOutcome.offer
        d) :
  d.dueByAirline.amount ≤
    Rules.OfferOrder.totalPaid payments
      o.id

A cancellation offer never makes the amount due by the airline larger than the payments received for the order.

Open question for the business. The offer is priced from the price of the order's live items, as in the worked examples, and the payments received do not enter it. A partly paid order is cancelled through an offer that returns its whole price. The example partlyPaidCancellation shows it: a 1,000.00 order with 300.00 received gets an offer of 1,000.00 due by the airline. Is the refundable amount capped at the payments received, and which route applies when some items are paid and others are not?

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

Checks acceptance criteria ONE-203.4.

15.2.5. Offer priced from live items🔗

guarantee

Rules.OneOrder.Change.offer_priced_from_live_items
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Change.ExcessPenalty) (o : Rules.OneOrder.Order)
  (payments : List Rules.OfferOrder.Payment)
  (t : Rules.OneOrder.Change.CancelTerms)
  (d : Rules.OneOrder.Change.PriceDifferential)
  (h :
    Rules.OneOrder.Change.requestCancellation m r o payments t =
      Rules.OneOrder.Change.CancelOutcome.offer d) :
  d.oldPrice.amount =
    (List.map (fun x ↦ x.price.amount)
        (Rules.OneOrder.Change.pricedItems o)).sum
Rules.OneOrder.Change.offer_priced_from_live_items
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.Change.ExcessPenalty)
  (o : Rules.OneOrder.Order)
  (payments :
    List Rules.OfferOrder.Payment)
  (t : Rules.OneOrder.Change.CancelTerms)
  (d :
    Rules.OneOrder.Change.PriceDifferential)
  (h :
    Rules.OneOrder.Change.requestCancellation
        m r o payments t =
      Rules.OneOrder.Change.CancelOutcome.offer
        d) :
  d.oldPrice.amount =
    (List.map (fun x ↦ x.price.amount)
        (Rules.OneOrder.Change.pricedItems
          o)).sum

A cancellation offer is priced from the order items that still hold a live service. An item whose services a change transferred or cancelled adds nothing, so its price is not returned a second time.

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

Checks acceptance criteria ONE-203.5.

15.3. Examples🔗

15.3.1. Unpaid cancellation while requested🔗

example

Rules.OneOrder.Change.unpaidCancellationWhileRequested :
  Option Rules.OneOrder.Change.ChangedOrder
Rules.OneOrder.Change.unpaidCancellationWhileRequested :
  Option
    Rules.OneOrder.Change.ChangedOrder

Given the trip order at 1,000.00 EUR with no payment received, its outbound flight confirmed and its inbound flight still REQUESTED from the airline.

When the seller asks to cancel it.

Then it is cancelled at once. The outbound service is cancelled and removed. The inbound service stays REQUESTED, because the delivery status table has no move from REQUESTED to REMOVED, so the item is not cancelled. Under the cautious reading the item is active; under the strict reading it has no status at all.

What Lean computed:

items item ORDITM-1, price 1000.00 EUR, cautious active, strict none, services item ORDITM-1, service SVC-OUT, status cancelled, delivery removed, item ORDITM-1, service SVC-IN, status requested, delivery requested

Checks acceptance criteria ONE-203.1, ONE-203.2, ONE-002.4.

15.3.2. Unpaid cancellation🔗

example

Rules.OneOrder.Change.unpaidCancellation :
  Rules.OneOrder.Change.CancelSummary
Rules.OneOrder.Change.unpaidCancellation :
  Rules.OneOrder.Change.CancelSummary

Given the trip order at 1,000.00 EUR, confirmed and waiting for payment, with no payment received.

When the seller asks to cancel it.

Then it is cancelled at once, with no offer and nothing due. Every service is cancelled and removed, and the order is closed under both readings.

What Lean computed:

Received: 0.00 EUR
Route: at once
Due by airline: 0.00 EUR
Order status: cautious closed, strict closed

Checks acceptance criteria ONE-203.1, ONE-203.2.

15.3.3. Paid cancellation🔗

example

Rules.OneOrder.Change.paidCancellation :
  Rules.OneOrder.Change.CancelSummary
Rules.OneOrder.Change.paidCancellation :
  Rules.OneOrder.Change.CancelSummary

Given the trip order at 1,000.00 EUR, paid in full and ready to proceed, with a cancellation penalty of 50.00 EUR netted and 20.00 EUR forfeited.

When the seller asks to cancel it.

Then it needs a cancellation offer, which refunds 930.00 EUR. The order stays opened until the seller accepts the offer.

What Lean computed:

Received: 1000.00 EUR
Route: through offer
Due by airline: 930.00 EUR
Order status: cautious opened, strict opened

Checks acceptance criteria ONE-203.3.

15.3.4. Partly paid cancellation🔗

example

Rules.OneOrder.Change.partlyPaidCancellation :
  Rules.OneOrder.Change.CancelSummary
Rules.OneOrder.Change.partlyPaidCancellation :
  Rules.OneOrder.Change.CancelSummary

Given the trip order at 1,000.00 EUR, still waiting for full payment, with 300.00 EUR received, and no penalty or forfeit.

When the seller asks to cancel it.

Then it needs a cancellation offer, as for any order with a payment. The offer is priced from the order's price and has 1,000.00 EUR due by the airline, more than the 300.00 EUR received.

What Lean computed:

Received: 300.00 EUR
Route: through offer
Due by airline: 1000.00 EUR
Order status: cautious opened, strict opened

Checks acceptance criteria ONE-203.3, ONE-203.4.

15.3.5. Cancel after change🔗

example

Rules.OneOrder.Change.cancelAfterChange :
  Rules.OneOrder.Change.CancelSummary
Rules.OneOrder.Change.cancelAfterChange :
  Rules.OneOrder.Change.CancelSummary

Given the trip order, paid 1,000.00 EUR and ready to proceed, after a paid change that keeps the outbound flight and puts a new inbound flight in a new item at 900.00 EUR.

When the seller asks to cancel the order, with no penalty and nothing forfeited.

Then the offer is priced from the new item alone, the only item that still holds a live service, and has 900.00 EUR due by the airline. The original item, whose services are transferred or cancelled, adds nothing.

What Lean computed:

Received: 1000.00 EUR
Route: through offer
Due by airline: 900.00 EUR
Order status: cautious opened, strict opened

Checks acceptance criteria ONE-203.5.

15.4. Open question🔗

The guarantee Orders cancelled at once are closed is open: the example Unpaid cancellation while requested, Unpaid cancellation shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

15.5. Open question🔗

The guarantee Cancellation offers stay within payments is open: the example Partly paid cancellation shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.