Verified Air

9. Services that end without delivery🔗

Requirement ONE-102. Of its 6 acceptance criteria, 6 are proven.

🔗rule
Rules.OneOrder.Delivery.endService
  (m : Rules.OneOrder.Delivery.MoveReading) :
  Rules.OneOrder.DeliveryStatus →
    Rules.OneOrder.Delivery.DeliveryEvent →
      Option Rules.OneOrder.DeliveryStatus
Rules.OneOrder.Delivery.endService
  (m :
    Rules.OneOrder.Delivery.MoveReading) :
  Rules.OneOrder.DeliveryStatus →
    Rules.OneOrder.Delivery.DeliveryEvent →
      Option Rules.OneOrder.DeliveryStatus

EARS: When a service is cancelled, expires, is not claimed or cannot be delivered, the system shall move it to the delivery status that records why.

Story: As a revenue accountant, I want each service that ends without delivery to record why, so that I know whether its value is held, refunded or earned.

Acceptance criteria:

  • ONE-102.1: When a service that is CONFIRMED, READY TO PROCEED or READY TO DELIVER is cancelled, the system shall mark it REMOVED HOLD VALUE if the airline holds its value for reuse and REMOVED if not.

  • ONE-102.2: When the value held for a REMOVED HOLD VALUE service is refunded, moved to a value store or used in a change, the system shall mark it REMOVED, the only move out of REMOVED HOLD VALUE.

  • ONE-102.3: When the consumption time limit of a service that is CONFIRMED, READY TO PROCEED or READY TO DELIVER passes before the customer claims it, the system shall mark it EXPIRED.

  • ONE-102.4: When the passenger's own action or inaction, such as a no-show, prevents delivery of a service that is CONFIRMED, READY TO PROCEED or READY TO DELIVER, the system shall mark it NOT CLAIMED.

  • ONE-102.5: When legal, regulatory or force majeure constraints prevent delivery of a service that is CONFIRMED, READY TO PROCEED or READY TO DELIVER, the system shall mark it UNABLE TO DELIVER.

  • ONE-102.6: When the airline or its provider fails to deliver a service that is CONFIRMED, READY TO PROCEED, READY TO DELIVER or IN PROGRESS because of its own limits, the system shall mark it FAILED TO DELIVER.

Whether an IN PROGRESS service can be cancelled or end NOT CLAIMED is left to the reading. The result is the new status, or none when the event does not end the service.

9.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-102.1

Proven

Reusable cancellation, Cancellation before delivery

ONE-102.2

Proven

Held value after cancellation, Reusable cancellation

ONE-102.3

Proven

Outcomes of paid flight, Expiry of an unclaimed service

ONE-102.4

Proven

Outcomes of paid flight, Passenger no-show

ONE-102.5

Proven

Outcomes of paid flight, Delivery prevented by outside constraints

ONE-102.6

Proven

Outcomes of paid flight, Delivery failed by the airline or its provider

9.2. Guarantees🔗

9.2.1. Cancellation before delivery🔗

🔗guarantee
Rules.OneOrder.Delivery.cancel_removes
  (m : Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (hs :
    s = Rules.OneOrder.DeliveryStatus.confirmed ∨
      s = Rules.OneOrder.DeliveryStatus.readyToProceed ∨
        s = Rules.OneOrder.DeliveryStatus.readyToDeliver) :
  Rules.OneOrder.Delivery.move m s
        Rules.OneOrder.Delivery.DeliveryEvent.remove =
      some Rules.OneOrder.DeliveryStatus.removed ∧
    Rules.OneOrder.Delivery.move m s
        Rules.OneOrder.Delivery.DeliveryEvent.removeHoldValue =
      some Rules.OneOrder.DeliveryStatus.removedHoldValue
Rules.OneOrder.Delivery.cancel_removes
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (hs :
    s =
        Rules.OneOrder.DeliveryStatus.confirmed ∨
      s =
          Rules.OneOrder.DeliveryStatus.readyToProceed ∨
        s =
          Rules.OneOrder.DeliveryStatus.readyToDeliver) :
  Rules.OneOrder.Delivery.move m s
        Rules.OneOrder.Delivery.DeliveryEvent.remove =
      some
        Rules.OneOrder.DeliveryStatus.removed ∧
    Rules.OneOrder.Delivery.move m s
        Rules.OneOrder.Delivery.DeliveryEvent.removeHoldValue =
      some
        Rules.OneOrder.DeliveryStatus.removedHoldValue

A service that is CONFIRMED, READY TO PROCEED or READY TO DELIVER becomes REMOVED when it is cancelled with none of its value kept, and REMOVED HOLD VALUE when the airline holds its value, under every reading.

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

Checks acceptance criteria ONE-102.1.

9.2.2. Held value after cancellation🔗

🔗guarantee
Rules.OneOrder.Delivery.held_value_only_released
  (m : Rules.OneOrder.Delivery.MoveReading)
  (before : Option Rules.OneOrder.DeliveryStatus)
  (e : Rules.OneOrder.Delivery.DeliveryEvent)
  (r : Rules.OneOrder.Delivery.DeliveryRecord) :
  Rules.OneOrder.Delivery.step m
        { status := Rules.OneOrder.DeliveryStatus.removedHoldValue,
          suspendedFrom := before }
        e =
      some r ↔
    e = Rules.OneOrder.Delivery.DeliveryEvent.releaseValue ∧
      r =
        { status := Rules.OneOrder.DeliveryStatus.removed,
          suspendedFrom := none }
Rules.OneOrder.Delivery.held_value_only_released
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (before :
    Option Rules.OneOrder.DeliveryStatus)
  (e :
    Rules.OneOrder.Delivery.DeliveryEvent)
  (r :
    Rules.OneOrder.Delivery.DeliveryRecord) :
  Rules.OneOrder.Delivery.step m
        {
          status :=
            Rules.OneOrder.DeliveryStatus.removedHoldValue,
          suspendedFrom := before }
        e =
      some r ↔
    e =
        Rules.OneOrder.Delivery.DeliveryEvent.releaseValue ∧
      r =
        {
          status :=
            Rules.OneOrder.DeliveryStatus.removed,
          suspendedFrom := none }

The only event a REMOVED HOLD VALUE service accepts is the release of its value, which makes it REMOVED, under every reading.

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

Checks acceptance criteria ONE-102.2.

9.2.3. Expiry of an unclaimed service🔗

🔗guarantee
Rules.OneOrder.Delivery.expire_marks_expired
  (m : Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (hs :
    s = Rules.OneOrder.DeliveryStatus.confirmed ∨
      s = Rules.OneOrder.DeliveryStatus.readyToProceed ∨
        s = Rules.OneOrder.DeliveryStatus.readyToDeliver) :
  Rules.OneOrder.Delivery.move m s
      Rules.OneOrder.Delivery.DeliveryEvent.expire =
    some Rules.OneOrder.DeliveryStatus.expired
Rules.OneOrder.Delivery.expire_marks_expired
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (hs :
    s =
        Rules.OneOrder.DeliveryStatus.confirmed ∨
      s =
          Rules.OneOrder.DeliveryStatus.readyToProceed ∨
        s =
          Rules.OneOrder.DeliveryStatus.readyToDeliver) :
  Rules.OneOrder.Delivery.move m s
      Rules.OneOrder.Delivery.DeliveryEvent.expire =
    some
      Rules.OneOrder.DeliveryStatus.expired

A service that is CONFIRMED, READY TO PROCEED or READY TO DELIVER becomes EXPIRED when its consumption time limit passes, under every reading.

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

Checks acceptance criteria ONE-102.3.

9.2.4. Passenger no-show🔗

🔗guarantee
Rules.OneOrder.Delivery.no_show_marks_not_claimed
  (m : Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (hs :
    s = Rules.OneOrder.DeliveryStatus.confirmed ∨
      s = Rules.OneOrder.DeliveryStatus.readyToProceed ∨
        s = Rules.OneOrder.DeliveryStatus.readyToDeliver) :
  Rules.OneOrder.Delivery.move m s
      Rules.OneOrder.Delivery.DeliveryEvent.notClaimed =
    some Rules.OneOrder.DeliveryStatus.notClaimed
Rules.OneOrder.Delivery.no_show_marks_not_claimed
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (hs :
    s =
        Rules.OneOrder.DeliveryStatus.confirmed ∨
      s =
          Rules.OneOrder.DeliveryStatus.readyToProceed ∨
        s =
          Rules.OneOrder.DeliveryStatus.readyToDeliver) :
  Rules.OneOrder.Delivery.move m s
      Rules.OneOrder.Delivery.DeliveryEvent.notClaimed =
    some
      Rules.OneOrder.DeliveryStatus.notClaimed

A service that is CONFIRMED, READY TO PROCEED or READY TO DELIVER becomes NOT CLAIMED when the passenger prevents its delivery, under every reading.

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

Checks acceptance criteria ONE-102.4.

9.2.5. Delivery prevented by outside constraints🔗

🔗guarantee
Rules.OneOrder.Delivery.unable_marks_unable
  (m : Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (hs :
    s = Rules.OneOrder.DeliveryStatus.confirmed ∨
      s = Rules.OneOrder.DeliveryStatus.readyToProceed ∨
        s = Rules.OneOrder.DeliveryStatus.readyToDeliver) :
  Rules.OneOrder.Delivery.move m s
      Rules.OneOrder.Delivery.DeliveryEvent.unable =
    some Rules.OneOrder.DeliveryStatus.unableToDeliver
Rules.OneOrder.Delivery.unable_marks_unable
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (hs :
    s =
        Rules.OneOrder.DeliveryStatus.confirmed ∨
      s =
          Rules.OneOrder.DeliveryStatus.readyToProceed ∨
        s =
          Rules.OneOrder.DeliveryStatus.readyToDeliver) :
  Rules.OneOrder.Delivery.move m s
      Rules.OneOrder.Delivery.DeliveryEvent.unable =
    some
      Rules.OneOrder.DeliveryStatus.unableToDeliver

A service that is CONFIRMED, READY TO PROCEED or READY TO DELIVER becomes UNABLE TO DELIVER when legal, regulatory or force majeure constraints prevent its delivery, under every reading.

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

Checks acceptance criteria ONE-102.5.

9.2.6. Delivery failed by the airline or its provider🔗

🔗guarantee
Rules.OneOrder.Delivery.fail_marks_failed
  (m : Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (hs :
    s = Rules.OneOrder.DeliveryStatus.confirmed ∨
      s = Rules.OneOrder.DeliveryStatus.readyToProceed ∨
        s = Rules.OneOrder.DeliveryStatus.readyToDeliver ∨
          s = Rules.OneOrder.DeliveryStatus.inProgress) :
  Rules.OneOrder.Delivery.move m s
      Rules.OneOrder.Delivery.DeliveryEvent.fail =
    some Rules.OneOrder.DeliveryStatus.failedToDeliver
Rules.OneOrder.Delivery.fail_marks_failed
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (hs :
    s =
        Rules.OneOrder.DeliveryStatus.confirmed ∨
      s =
          Rules.OneOrder.DeliveryStatus.readyToProceed ∨
        s =
            Rules.OneOrder.DeliveryStatus.readyToDeliver ∨
          s =
            Rules.OneOrder.DeliveryStatus.inProgress) :
  Rules.OneOrder.Delivery.move m s
      Rules.OneOrder.Delivery.DeliveryEvent.fail =
    some
      Rules.OneOrder.DeliveryStatus.failedToDeliver

A service that is CONFIRMED, READY TO PROCEED, READY TO DELIVER or IN PROGRESS becomes FAILED TO DELIVER when the airline or its provider fails to deliver it, under every reading.

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

Checks acceptance criteria ONE-102.6.

9.3. Examples🔗

9.3.1. Reusable cancellation🔗

🔗example
Rules.OneOrder.Delivery.reusableCancellation :
  Rules.OneOrder.Delivery.HeldValue
Rules.OneOrder.Delivery.reusableCancellation :
  Rules.OneOrder.Delivery.HeldValue

Given an order whose one service is a paid bag, READY TO PROCEED.

When the customer cancels the bag and the airline holds its value for reuse, and later the value is refunded.

Then the bag is REMOVED HOLD VALUE and the order stays opened while the value is held. Once the value is refunded the bag is REMOVED and the order is closed. Both hold under either reading of the guide.

What Lean computed:

  • After cancellation: removed hold value

  • Order while held: cautious opened, strict opened

  • After release: removed

  • Order after release: cautious closed, strict closed

Checks acceptance criteria ONE-102.1, ONE-102.2.

9.3.2. Outcomes of paid flight🔗

🔗example
Rules.OneOrder.Delivery.outcomesOfPaidFlight :
  List Rules.OneOrder.Delivery.Outcome
Rules.OneOrder.Delivery.outcomesOfPaidFlight :
  List Rules.OneOrder.Delivery.Outcome

Given a paid flight service, READY TO PROCEED.

When its consumption time limit passes, or the passenger does not show, or a force majeure event prevents the flight, or the airline fails to operate it.

Then the flight becomes EXPIRED, NOT CLAIMED, UNABLE TO DELIVER or FAILED TO DELIVER. The guide does not say whether any of these holds value: under the cautious reading each does, and under the strict reading none does.

What Lean computed:

Event

Status

Cautious holds value

Strict holds value

expire

expired

yes

no

not claimed

not claimed

yes

no

unable

unable to deliver

yes

no

fail

failed to deliver

yes

no

Checks acceptance criteria ONE-102.3, ONE-102.4, ONE-102.5, ONE-102.6.