10. Final delivery statuses🔗

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

rule

Rules.OneOrder.Delivery.isFinal : Rules.OneOrder.DeliveryStatus → Bool
Rules.OneOrder.Delivery.isFinal :
  Rules.OneOrder.DeliveryStatus → Bool

EARS: The system shall treat DELIVERED, REMOVED, EXPIRED, NOT CLAIMED and FAILED TO DELIVER as final delivery statuses, which no event leaves.

Story: As a revenue accountant, I want a service's final delivery status never to change, so that what accounting was told about the service stays true.

Acceptance criteria:

ONE-103.1: If a service is DELIVERED, REMOVED, EXPIRED, NOT CLAIMED or FAILED TO DELIVER, then the system shall refuse every event for its delivery status.
ONE-103.2: The system shall let every service that is not in a final delivery status reach one through some sequence of events.
ONE-103.3: While an order is closed, the system shall refuse every event for the delivery status of its services.
ONE-103.4: When every service of an order is in a final delivery status, the system shall mark the order closed.

These are the five statuses the accounting message names as final. UNABLE TO DELIVER is not among them, and the sources do not say whether it is final.

10.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-103.1	Proven	Events accepted, No event leaves a final status
ONE-103.2	Proven	Unable to deliver way out, Every service can reach a final status
ONE-103.3	Proven	Closed orders keep their delivery statuses, Closed order events
ONE-103.4	Open	No show order, Orders whose services are all final are closed, Failed delivery order

10.2. Guarantees🔗

10.2.1. No event leaves a final status🔗

guarantee

Rules.OneOrder.Delivery.final_refuses_all
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Delivery.DeliveryRecord)
  (e : Rules.OneOrder.Delivery.DeliveryEvent)
  (h : Rules.OneOrder.Delivery.isFinal r.status = true) :
  Rules.OneOrder.Delivery.step m r e = none
Rules.OneOrder.Delivery.final_refuses_all
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.Delivery.DeliveryRecord)
  (e :
    Rules.OneOrder.Delivery.DeliveryEvent)
  (h :
    Rules.OneOrder.Delivery.isFinal
        r.status =
      true) :
  Rules.OneOrder.Delivery.step m r e =
    none

No event moves a service out of a final delivery status, under every reading: not a delivery, a cancellation or a suspension.

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

Checks acceptance criteria ONE-103.1.

10.2.2. Every service can reach a final status🔗

guarantee

Rules.OneOrder.Delivery.final_reachable
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Delivery.DeliveryRecord)
  (h : Rules.OneOrder.Delivery.isFinal r.status = false) :
  ∃ es,
    Rules.OneOrder.Delivery.isFinal
        (Rules.OneOrder.Delivery.run m r es).status =
      true
Rules.OneOrder.Delivery.final_reachable
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.Delivery.DeliveryRecord)
  (h :
    Rules.OneOrder.Delivery.isFinal
        r.status =
      false) :
  ∃ es,
    Rules.OneOrder.Delivery.isFinal
        (Rules.OneOrder.Delivery.run m r
            es).status =
      true

Every service that is not in a final delivery status can reach one, under every reading. For an UNABLE TO DELIVER service, under a reading where it does not return to READY TO PROCEED, the only way is to suspend it and then remove it.

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

Checks acceptance criteria ONE-103.2.

10.2.3. Closed orders keep their delivery statuses🔗

guarantee

Rules.OneOrder.Delivery.closed_order_refuses_events
  (m : Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading) (o : Rules.OneOrder.Order)
  (h :
    Rules.OneOrder.OrderStatus.closed ∈
      Rules.OneOrder.orderStatuses v o)
  (i : Rules.OneOrder.OrderItem) (hi : i ∈ o.items)
  (s : Rules.OneOrder.Service) (hs : s ∈ i.services)
  (before : Option Rules.OneOrder.DeliveryStatus)
  (e : Rules.OneOrder.Delivery.DeliveryEvent) :
  Rules.OneOrder.Delivery.step m
      { status := s.delivery, suspendedFrom := before } e =
    none
Rules.OneOrder.Delivery.closed_order_refuses_events
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order)
  (h :
    Rules.OneOrder.OrderStatus.closed ∈
      Rules.OneOrder.orderStatuses v o)
  (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ o.items)
  (s : Rules.OneOrder.Service)
  (hs : s ∈ i.services)
  (before :
    Option Rules.OneOrder.DeliveryStatus)
  (e :
    Rules.OneOrder.Delivery.DeliveryEvent) :
  Rules.OneOrder.Delivery.step m
      { status := s.delivery,
        suspendedFrom := before }
      e =
    none

No event changes the delivery status of a service in a closed order, under every reading of the sources and of the guide: a closed order's services are all DELIVERED or REMOVED, and both are final.

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

Checks acceptance criteria ONE-103.3.

10.2.4. Orders whose services are all final are closed🔗

guarantee

Rules.OneOrder.Delivery.all_final_order_closed
  (v : Rules.OneOrder.ValueReading) (o : Rules.OneOrder.Order)
  (hne : ∃ i ∈ o.items, i.services ≠ [])
  (h :
    ∀ i ∈ o.items,
      ∀ s ∈ i.services,
        Rules.OneOrder.Delivery.isFinal s.delivery = true) :
  Rules.OneOrder.orderStatuses v o = [Rules.OneOrder.OrderStatus.closed]
Rules.OneOrder.Delivery.all_final_order_closed
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order)
  (hne : ∃ i ∈ o.items, i.services ≠ [])
  (h :
    ∀ i ∈ o.items,
      ∀ s ∈ i.services,
        Rules.OneOrder.Delivery.isFinal
            s.delivery =
          true) :
  Rules.OneOrder.orderStatuses v o =
    [Rules.OneOrder.OrderStatus.closed]

An order whose services have all reached a final delivery status is closed, under every reading of the guide.

Open question for the business. The guide closes an order only when every service is DELIVERED or REMOVED. EXPIRED, NOT CLAIMED and FAILED TO DELIVER are final too, but an order whose services end in them is never closed. Under a reading where such a service holds value the order stays opened for good; under one where it holds none the order has no status. The examples noShowOrder and failedDeliveryOrder show it. Should an order close once every service is final, and do EXPIRED, NOT CLAIMED and FAILED TO DELIVER hold value?

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

Checks acceptance criteria ONE-103.4.

10.3. Examples🔗

10.3.1. Events accepted🔗

example

Rules.OneOrder.Delivery.eventsAccepted :
  List Rules.OneOrder.Delivery.StatusEvents
Rules.OneOrder.Delivery.eventsAccepted :
  List
    Rules.OneOrder.Delivery.StatusEvents

Given each delivery status but SUSPENDED, under the loose reading, where every move the sources leave undecided is allowed.

When each event happens to a service in it.

Then a service that is DELIVERED, REMOVED, EXPIRED, NOT CLAIMED or FAILED TO DELIVER accepts no event. Every other status accepts at least one.

What Lean computed:

Status	Accepts
requested	confirm, suspend
confirmed	pay, prepare, start, deliver, remove, remove hold value, expire, not claimed, unable, fail, suspend
ready to proceed	prepare, start, deliver, remove, remove hold value, expire, not claimed, unable, fail, suspend
ready to deliver	start, deliver, remove, remove hold value, expire, not claimed, unable, fail, suspend
in progress	deliver, remove, remove hold value, not claimed, fail, suspend
delivered	none
removed hold value	release value
removed	none
expired	none
not claimed	none
unable to deliver	constraint lifted, suspend
failed to deliver	none

Checks acceptance criteria ONE-103.1.

10.3.2. Unable to deliver way out🔗

example

Rules.OneOrder.Delivery.unableToDeliverWayOut :
  Rules.OneOrder.Delivery.WayOut
Rules.OneOrder.Delivery.unableToDeliverWayOut :
  Rules.OneOrder.Delivery.WayOut

Given a flight service that is UNABLE TO DELIVER because of a force majeure event.

When the events it accepts are listed under each reading, and the airline suspends it and then removes it.

Then under the strict reading its only accepted event is a suspension, so the only way to a final status is to suspend it and then remove it. Under the loose reading it can also return to READY TO PROCEED.

What Lean computed:

Strict accepts: suspend
Loose accepts: constraint lifted, suspend
After suspend and remove: removed

Checks acceptance criteria ONE-103.2.

10.3.3. Closed order events🔗

example

Rules.OneOrder.Delivery.closedOrderEvents :
  Rules.OneOrder.Delivery.ClosedOrder
Rules.OneOrder.Delivery.closedOrderEvents :
  Rules.OneOrder.Delivery.ClosedOrder

Given an order whose one item holds a delivered flight and a removed bag.

When each event happens to each of its services, under the loose reading of the sources.

Then the order is closed under both readings of the guide, and no event is accepted for either service.

What Lean computed:

Order status: cautious closed, strict closed
Accepts: none

Checks acceptance criteria ONE-103.3.

10.3.4. Failed delivery order🔗

example

Rules.OneOrder.Delivery.failedDeliveryOrder :
  Rules.OneOrder.OrderStatuses
Rules.OneOrder.Delivery.failedDeliveryOrder :
  Rules.OneOrder.OrderStatuses

Given an order whose one flight service is FAILED TO DELIVER because the airline could not operate the flight.

When the order's status is worked out.

Then the flight's status is final, but the order is not closed. Under the cautious reading it stays opened for good; under the strict reading it has no status, and the flight's value is gone with no refund.

What Lean computed:

Cautious: opened
Strict: none

Checks acceptance criteria ONE-103.4.

10.3.5. No show order🔗

example

Rules.OneOrder.Delivery.noShowOrder : Rules.OneOrder.OrderStatuses
Rules.OneOrder.Delivery.noShowOrder :
  Rules.OneOrder.OrderStatuses

Given an order whose one flight service is NOT CLAIMED because the passenger did not show.

When the order's status is worked out.

Then the flight's status is final, but the order is not closed. Under the cautious reading it stays opened, and since no event leaves NOT CLAIMED it stays opened for good. Under the strict reading it has no status.

What Lean computed:

Cautious: opened
Strict: none

Checks acceptance criteria ONE-103.4.

10.4. Open question🔗

The guarantee Orders whose services are all final are closed is open: the example Failed delivery order, No show order shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.