Verified Air

6. Order item status🔗

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

🔗rule
Rules.OneOrder.itemStatuses (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) : List Rules.OneOrder.ItemStatus
Rules.OneOrder.itemStatuses
  (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) :
  List Rules.OneOrder.ItemStatus

EARS: The system shall give each order item the status active, cancelled or closed from the service and delivery statuses of its services.

Story: As a revenue accountant, I want each order item's status worked out from its services, so that I know which items still hold value.

Acceptance criteria:

  • ONE-002.1: While at least one service of an order item holds value, the system shall mark the item active.

  • ONE-002.2: When every service of an order item is cancelled or transferred and none holds value, the system shall mark the item cancelled.

  • ONE-002.3: When at least one service of an order item is delivered and every other service is delivered or removed, the system shall mark the item closed.

  • ONE-002.4: The system shall give each order item exactly one status.

The result lists every status whose condition holds, so an item that meets two conditions, or none, shows it.

6.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-002.1

Proven

Active items are those holding value, Paid item

ONE-002.2

Proven

Cancelled items as the guide defines them, Cancelled item

ONE-002.3

Proven

Closed item, Closed items as the guide defines them

ONE-002.4

Open

Suspended service, Each item has exactly one status, Active items are never closed, Unpaid cancellation while requested, Delivered then transferred, Active items are never cancelled

6.2. Guarantees🔗

6.2.1. Active items are those holding value🔗

🔗guarantee
Rules.OneOrder.item_active_iff (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) :
  Rules.OneOrder.ItemStatus.active ∈ Rules.OneOrder.itemStatuses v i ↔
    ∃ s ∈ i.services, Rules.OneOrder.Service.holdsValue v s = true
Rules.OneOrder.item_active_iff
  (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) :
  Rules.OneOrder.ItemStatus.active ∈
      Rules.OneOrder.itemStatuses v i ↔
    ∃ s ∈ i.services,
      Rules.OneOrder.Service.holdsValue v
          s =
        true

An item is marked active exactly when at least one of its services holds value.

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

Checks acceptance criteria ONE-002.1.

6.2.2. Cancelled items as the guide defines them🔗

🔗guarantee
Rules.OneOrder.item_cancelled_iff (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) :
  Rules.OneOrder.ItemStatus.cancelled ∈
      Rules.OneOrder.itemStatuses v i ↔
    (∀ s ∈ i.services,
        s.status = Rules.OneOrder.ServiceStatus.cancelled ∨
          s.status = Rules.OneOrder.ServiceStatus.transferred) ∧
      ∀ s ∈ i.services, Rules.OneOrder.Service.holdsValue v s = false
Rules.OneOrder.item_cancelled_iff
  (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) :
  Rules.OneOrder.ItemStatus.cancelled ∈
      Rules.OneOrder.itemStatuses v i ↔
    (∀ s ∈ i.services,
        s.status =
            Rules.OneOrder.ServiceStatus.cancelled ∨
          s.status =
            Rules.OneOrder.ServiceStatus.transferred) ∧
      ∀ s ∈ i.services,
        Rules.OneOrder.Service.holdsValue
            v s =
          false

An item is marked cancelled exactly when every service is cancelled or transferred and none holds value.

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

Checks acceptance criteria ONE-002.2.

6.2.3. Closed items as the guide defines them🔗

🔗guarantee
Rules.OneOrder.item_closed_iff (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) :
  Rules.OneOrder.ItemStatus.closed ∈ Rules.OneOrder.itemStatuses v i ↔
    (∃ s ∈ i.services,
        s.delivery = Rules.OneOrder.DeliveryStatus.delivered) ∧
      ∀ s ∈ i.services,
        s.delivery = Rules.OneOrder.DeliveryStatus.delivered ∨
          s.delivery = Rules.OneOrder.DeliveryStatus.removed
Rules.OneOrder.item_closed_iff
  (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) :
  Rules.OneOrder.ItemStatus.closed ∈
      Rules.OneOrder.itemStatuses v i ↔
    (∃ s ∈ i.services,
        s.delivery =
          Rules.OneOrder.DeliveryStatus.delivered) ∧
      ∀ s ∈ i.services,
        s.delivery =
            Rules.OneOrder.DeliveryStatus.delivered ∨
          s.delivery =
            Rules.OneOrder.DeliveryStatus.removed

An item is marked closed exactly when at least one service is delivered and every service is delivered or removed.

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

Checks acceptance criteria ONE-002.3.

6.2.4. Active items are never cancelled🔗

🔗guarantee
Rules.OneOrder.active_not_cancelled (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) :
  ¬(Rules.OneOrder.OrderItem.isActive v i = true ∧
      Rules.OneOrder.OrderItem.isCancelled v i = true)
Rules.OneOrder.active_not_cancelled
  (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) :
  ¬(Rules.OneOrder.OrderItem.isActive v
          i =
        true ∧
      Rules.OneOrder.OrderItem.isCancelled
          v i =
        true)

An active item is never cancelled: the cancelled status requires that no service holds value.

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

Checks acceptance criteria ONE-002.4.

6.2.5. Active items are never closed🔗

🔗guarantee
Rules.OneOrder.active_not_closed (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) :
  ¬(Rules.OneOrder.OrderItem.isActive v i = true ∧ i.isClosed = true)
Rules.OneOrder.active_not_closed
  (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) :
  ¬(Rules.OneOrder.OrderItem.isActive v
          i =
        true ∧
      i.isClosed = true)

An active item is never closed, under every reading of the guide: a closed item's services are all delivered or removed, and neither holds value.

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

Checks acceptance criteria ONE-002.4.

6.2.6. Each item has exactly one status🔗

🔗guarantee
Rules.OneOrder.item_has_one_status (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem) (h : i.services ≠ []) :
  (Rules.OneOrder.itemStatuses v i).length = 1
Rules.OneOrder.item_has_one_status
  (v : Rules.OneOrder.ValueReading)
  (i : Rules.OneOrder.OrderItem)
  (h : i.services ≠ []) :
  (Rules.OneOrder.itemStatuses v
        i).length =
    1

Each order item has exactly one status, active, cancelled or closed.

Open question for the business. The guide's three conditions overlap and leave gaps. An item whose one service was delivered and then transferred to another item meets both the cancelled condition (every service transferred, none holding value) and the closed condition (a service delivered, the rest delivered or removed). The example deliveredThenTransferred shows it. Which status wins, and should a delivered service be transferable at all?

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

Checks acceptance criteria ONE-002.4.

6.3. Examples🔗

6.3.1. Paid item🔗

🔗example
Rules.OneOrder.paidItem : Rules.OneOrder.ItemStatuses
Rules.OneOrder.paidItem :
  Rules.OneOrder.ItemStatuses

Given an order item with one flight service, paid for and ready to proceed.

When the item's status is worked out.

Then it is active under both readings, since a service ready to proceed holds value.

What Lean computed:

  • Cautious: active

  • Strict: active

Checks acceptance criteria ONE-002.1.

6.3.2. Cancelled item🔗

🔗example
Rules.OneOrder.cancelledItem : Rules.OneOrder.ItemStatuses
Rules.OneOrder.cancelledItem :
  Rules.OneOrder.ItemStatuses

Given an order item whose one flight service was cancelled and removed, with no value kept.

When the item's status is worked out.

Then it is cancelled under both readings.

What Lean computed:

  • Cautious: cancelled

  • Strict: cancelled

Checks acceptance criteria ONE-002.2.

6.3.3. Closed item🔗

🔗example
Rules.OneOrder.closedItem : Rules.OneOrder.ItemStatuses
Rules.OneOrder.closedItem :
  Rules.OneOrder.ItemStatuses

Given an order item with two services: a flight that was delivered and a bag that was removed.

When the item's status is worked out.

Then it is closed under both readings.

What Lean computed:

  • Cautious: closed

  • Strict: closed

Checks acceptance criteria ONE-002.3.

6.3.4. 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.

6.3.5. Delivered then transferred🔗

🔗example
Rules.OneOrder.deliveredThenTransferred : Rules.OneOrder.ItemStatuses
Rules.OneOrder.deliveredThenTransferred :
  Rules.OneOrder.ItemStatuses

Given an order item whose one flight service was delivered and then transferred to another order item by a change.

When the item's status is worked out.

Then it is both cancelled and closed under both readings. The guide's cancelled condition (every service transferred, none holding value) and its closed condition (a service delivered, the rest delivered or removed) both hold.

What Lean computed:

  • Cautious: cancelled, closed

  • Strict: cancelled, closed

Checks acceptance criteria ONE-002.4.

6.3.6. Suspended service🔗

🔗example
Rules.OneOrder.suspendedService : Rules.OneOrder.ItemStatuses
Rules.OneOrder.suspendedService :
  Rules.OneOrder.ItemStatuses

Given an order item whose one flight service is suspended by an airline decision.

When the item's status is worked out.

Then under the cautious reading it is active. Under the strict reading it has no status: the service holds no value, is neither cancelled nor transferred, and was not delivered.

What Lean computed:

  • Cautious: active

  • Strict: none

Checks acceptance criteria ONE-002.4.

6.4. Open question🔗

The guarantee Each item has exactly one status is open: the example Unpaid cancellation while requested, Delivered then transferred, Suspended service shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.