Verified Air

13. Price differential of a change🔗

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

🔗rule
Rules.OneOrder.Change.priceDifferential (r : Rules.OneOrder.Change.ExcessPenalty) (q : Rules.OneOrder.Change.ChangeQuote) : Except Rules.OneOrder.Change.QuoteRejection Rules.OneOrder.Change.PriceDifferential
Rules.OneOrder.Change.priceDifferential (r : Rules.OneOrder.Change.ExcessPenalty) (q : Rules.OneOrder.Change.ChangeQuote) : Except Rules.OneOrder.Change.QuoteRejection Rules.OneOrder.Change.PriceDifferential

EARS: When the airline prices a change or cancellation of order items, the system shall state the amount due to the airline, the amount due by the airline and a type code that names the outcome.

Story: As a seller, I want every change or cancellation offer to state what the customer pays and what the airline returns, so that I can settle the change without working the amounts out myself.

Acceptance criteria:

  • ONE-201.1: If the prices, penalty and forfeited amount of a change are not all in one currency, then the system shall reject the change unpriced.

  • ONE-201.2: The system shall give a price differential a type code that names a collection exactly when an amount is due to the airline.

  • ONE-201.3: The system shall give a price differential a type code that names a refund or a value store exactly when an amount is due by the airline.

  • ONE-201.4: When the seller asks to keep the value of cancelled items for later use, the system shall type the differential Reusable and set both due amounts to zero.

  • ONE-201.5: When the airline prices a change or cancellation, the system shall make the amount due to the airline less the amount due by the airline equal the new price, less the old price, plus the penalty, plus the forfeited amount.

The due amounts come from dueAmounts, except for a request to keep the value for later use, where the guide shows both amounts as zero (statedDue).

13.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-201.1

Proven

Mixed currency change, Mixed currencies are rejected

ONE-201.2

Proven

Type code names a collection, Penalty netted or separate, Change with collection

ONE-201.3

Proven

Type code names a refund or a value store, Penalty netted or separate, Cancellation with forfeit

ONE-201.4

Proven

Value kept for later use is typed Reusable, Respend cancellation

ONE-201.5

Open

Penalty above refund, Respend cancellation, Due amounts net to the difference

13.2. Guarantees🔗

13.2.1. Mixed currencies are rejected🔗

🔗guarantee
Rules.OneOrder.Change.differential_rejects_mixed_currency (r : Rules.OneOrder.Change.ExcessPenalty) (q : Rules.OneOrder.Change.ChangeQuote) (h : q.newPrice.currency ≠ q.oldPrice.currency ∨ q.penalty.currency ≠ q.oldPrice.currency ∨ q.forfeited.currency ≠ q.oldPrice.currency) : Rules.OneOrder.Change.priceDifferential r q = Except.error Rules.OneOrder.Change.QuoteRejection.mixedCurrency
Rules.OneOrder.Change.differential_rejects_mixed_currency (r : Rules.OneOrder.Change.ExcessPenalty) (q : Rules.OneOrder.Change.ChangeQuote) (h : q.newPrice.currency ≠ q.oldPrice.currency ∨ q.penalty.currency ≠ q.oldPrice.currency ∨ q.forfeited.currency ≠ q.oldPrice.currency) : Rules.OneOrder.Change.priceDifferential r q = Except.error Rules.OneOrder.Change.QuoteRejection.mixedCurrency

A change whose amounts are not all in one currency is rejected unpriced.

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

Checks acceptance criteria ONE-201.1.

13.2.2. Type code names a collection🔗

🔗guarantee
Rules.OneOrder.Change.differential_collects_iff (r : Rules.OneOrder.Change.ExcessPenalty) (q : Rules.OneOrder.Change.ChangeQuote) (d : Rules.OneOrder.Change.PriceDifferential) (h : Rules.OneOrder.Change.priceDifferential r q = Except.ok d) : d.type.collects = true ↔ 0 < d.dueToAirline.amount
Rules.OneOrder.Change.differential_collects_iff (r : Rules.OneOrder.Change.ExcessPenalty) (q : Rules.OneOrder.Change.ChangeQuote) (d : Rules.OneOrder.Change.PriceDifferential) (h : Rules.OneOrder.Change.priceDifferential r q = Except.ok d) : d.type.collects = true ↔ 0 < d.dueToAirline.amount

A type code names a collection exactly when an amount is due to the airline.

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

Checks acceptance criteria ONE-201.2.

13.2.3. Type code names a refund or a value store🔗

🔗guarantee
Rules.OneOrder.Change.differential_pays_iff (r : Rules.OneOrder.Change.ExcessPenalty) (q : Rules.OneOrder.Change.ChangeQuote) (d : Rules.OneOrder.Change.PriceDifferential) (h : Rules.OneOrder.Change.priceDifferential r q = Except.ok d) : d.type.pays = true ↔ 0 < d.dueByAirline.amount
Rules.OneOrder.Change.differential_pays_iff (r : Rules.OneOrder.Change.ExcessPenalty) (q : Rules.OneOrder.Change.ChangeQuote) (d : Rules.OneOrder.Change.PriceDifferential) (h : Rules.OneOrder.Change.priceDifferential r q = Except.ok d) : d.type.pays = true ↔ 0 < d.dueByAirline.amount

A type code names a refund or a value store exactly when an amount is due by the airline.

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

Checks acceptance criteria ONE-201.3.

13.2.4. Value kept for later use is typed Reusable🔗

🔗guarantee
Rules.OneOrder.Change.respend_reusable (r : Rules.OneOrder.Change.ExcessPenalty) (q : Rules.OneOrder.Change.ChangeQuote) (d : Rules.OneOrder.Change.PriceDifferential) (h : Rules.OneOrder.Change.priceDifferential r q = Except.ok d) (hs : q.settlement = Rules.OneOrder.Change.Settlement.respend) : d.type = Rules.OneOrder.Change.DifferentialType.reusable ∧ d.dueToAirline.amount = 0 ∧ d.dueByAirline.amount = 0
Rules.OneOrder.Change.respend_reusable (r : Rules.OneOrder.Change.ExcessPenalty) (q : Rules.OneOrder.Change.ChangeQuote) (d : Rules.OneOrder.Change.PriceDifferential) (h : Rules.OneOrder.Change.priceDifferential r q = Except.ok d) (hs : q.settlement = Rules.OneOrder.Change.Settlement.respend) : d.type = Rules.OneOrder.Change.DifferentialType.reusable ∧ d.dueToAirline.amount = 0 ∧ d.dueByAirline.amount = 0

When the seller asks to keep the value of cancelled items for later use, the differential is typed Reusable and both due amounts are zero.

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

Checks acceptance criteria ONE-201.4.

13.2.5. Due amounts net to the difference🔗

🔗guarantee
Rules.OneOrder.Change.differential_nets (r : Rules.OneOrder.Change.ExcessPenalty) (q : Rules.OneOrder.Change.ChangeQuote) (d : Rules.OneOrder.Change.PriceDifferential) (h : Rules.OneOrder.Change.priceDifferential r q = Except.ok d) : ↑d.dueToAirline.amount - ↑d.dueByAirline.amount = ↑q.newPrice.amount - ↑q.oldPrice.amount + ↑q.penalty.amount + ↑q.forfeited.amount
Rules.OneOrder.Change.differential_nets (r : Rules.OneOrder.Change.ExcessPenalty) (q : Rules.OneOrder.Change.ChangeQuote) (d : Rules.OneOrder.Change.PriceDifferential) (h : Rules.OneOrder.Change.priceDifferential r q = Except.ok d) : ↑d.dueToAirline.amount - ↑d.dueByAirline.amount = ↑q.newPrice.amount - ↑q.oldPrice.amount + ↑q.penalty.amount + ↑q.forfeited.amount

For every change or cancellation the airline prices, the amount due to the airline less the amount due by the airline is the new price, less the old price, plus the penalty, plus the forfeited amount.

Open question for the business. Two cases break it. When the seller asks to keep the value of cancelled items for later use, the guide shows both due amounts as zero, while the formula gives the whole refundable value as due by the airline; the example respendCancellation shows it. Under the reading that waives a penalty above the refundable value, the airline charges less than the penalty, so the formula overstates what the customer pays; the example penaltyAboveRefund shows it. Should the value held for later use count as the new price, and is a penalty above the refundable value collected or waived?

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

Checks acceptance criteria ONE-201.5.

13.3. Examples🔗

13.3.1. Mixed currency change🔗

🔗example
Rules.OneOrder.Change.mixedCurrencyChange : Except Rules.OneOrder.Change.QuoteRejection Rules.OneOrder.Change.PriceDifferential
Rules.OneOrder.Change.mixedCurrencyChange : Except Rules.OneOrder.Change.QuoteRejection Rules.OneOrder.Change.PriceDifferential

Given a change priced in euros whose penalty is stated in US dollars. The guide's sample change record shows a similar mismatch between the currency of its prices and that of its due amount.

When the airline prices the change.

Then the change is rejected unpriced.

What Lean computed:

Rejected: mixed currency.

Checks acceptance criteria ONE-201.1.

13.3.2. Change with collection🔗

🔗example
Rules.OneOrder.Change.changeWithCollection : List Rules.OneOrder.Change.PricedCase
Rules.OneOrder.Change.changeWithCollection : List Rules.OneOrder.Change.PricedCase

Given a paid trip at 1,000.00 EUR, of which 120.00 EUR is forfeited, changed to a trip at 900.00 EUR with a penalty of 40.00 EUR netted. These are the figures of worked example EXM_ORD_003C.

When the airline prices the change.

Then the customer pays 60.00 EUR, the airline returns nothing, and the type code is AddCol, as in the worked example.

What Lean computed:

Case

Due to airline

Due by airline

Type

change to a cheaper trip

60.00 EUR

0.00 EUR

add col

Checks acceptance criteria ONE-201.2, ONE-202.1.

13.3.3. Penalty netted or separate🔗

🔗example
Rules.OneOrder.Change.penaltyNettedOrSeparate : List Rules.OneOrder.Change.PricedCase
Rules.OneOrder.Change.penaltyNettedOrSeparate : List Rules.OneOrder.Change.PricedCase

Given a paid trip at 1,000.00 EUR changed to a trip at 840.00 EUR with a penalty of 60.00 EUR, where the airline keeps what it owes in a value store. The amounts due match worked example EXM_ORD_003G.

When the airline prices the change with the penalty netted, and again with the penalty charged separately.

Then netted, the customer pays nothing and 100.00 EUR goes to a value store. Charged separately, the customer pays 60.00 EUR and 160.00 EUR goes to a value store. Either way the customer is 100.00 EUR better off.

What Lean computed:

Case

Due to airline

Due by airline

Type

penalty netted

0.00 EUR

100.00 EUR

residual

penalty charged separately

60.00 EUR

160.00 EUR

add col and residual

Checks acceptance criteria ONE-201.2, ONE-201.3, ONE-202.2, ONE-202.3.

13.3.4. Cancellation with forfeit🔗

🔗example
Rules.OneOrder.Change.cancellationWithForfeit : List Rules.OneOrder.Change.PricedCase
Rules.OneOrder.Change.cancellationWithForfeit : List Rules.OneOrder.Change.PricedCase

Given a paid order at 1,000.00 EUR, of which 20.00 EUR is forfeited, cancelled with a penalty of 50.00 EUR netted and a refund. These are the figures of worked example EXM_ORD_030B.

When the airline prices the cancellation.

Then the airline refunds 930.00 EUR and the type code is Refund, as in the worked example.

What Lean computed:

Case

Due to airline

Due by airline

Type

cancellation

0.00 EUR

930.00 EUR

refund

Checks acceptance criteria ONE-201.3, ONE-202.1.

13.3.5. Respend cancellation🔗

🔗example
Rules.OneOrder.Change.respendCancellation : List Rules.OneOrder.Change.FormulaCase
Rules.OneOrder.Change.respendCancellation : List Rules.OneOrder.Change.FormulaCase

Given a paid order at 1,000.00 EUR, cancelled with no penalty and no forfeit, where the seller asks to keep the value for later use. This is worked example EXM_ORD_030E.

When the airline prices the cancellation.

Then the differential is typed Reusable with both due amounts zero, as in the worked example. The formula of ONE-201.5 requires 1,000.00 EUR due by the airline.

What Lean computed:

Case

Due to airline

Due by airline

Type

Formula to airline

Formula by airline

keep the value for later use

0.00 EUR

0.00 EUR

reusable

0.00 EUR

1000.00 EUR

Checks acceptance criteria ONE-201.4, ONE-201.5.

13.3.6. Penalty above refund🔗

🔗example
Rules.OneOrder.Change.penaltyAboveRefund : List Rules.OneOrder.Change.FormulaCase
Rules.OneOrder.Change.penaltyAboveRefund : List Rules.OneOrder.Change.FormulaCase

Given the cancellation of worked example EXM_ORD_030B (a paid order at 1,000.00 EUR with 20.00 EUR forfeited) with a penalty of 1,000.00 EUR netted in place of 50.00 EUR. The refundable value is 980.00 EUR, less than the penalty.

When the airline prices the cancellation under each reading of the guide.

Then under the reading that collects the whole penalty, the customer owes 20.00 EUR on a cancellation. Under the reading that waives the excess, nothing is due either way, while the formula of ONE-201.5 requires 20.00 EUR due to the airline.

What Lean computed:

Case

Due to airline

Due by airline

Type

Formula to airline

Formula by airline

collect the whole penalty

20.00 EUR

0.00 EUR

add col

20.00 EUR

0.00 EUR

waive the excess

0.00 EUR

0.00 EUR

even exchange

20.00 EUR

0.00 EUR

Checks acceptance criteria ONE-201.5, ONE-202.4.

13.4. Open question🔗

The guarantee Due amounts net to the difference is open: the example Respend cancellation, Penalty above refund shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.