AtomicPayment

Pure cost extraction plus an original isolated payment teaching model.

Package payment, input revision 3. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

BaseCost · constant

payment · input revision 3 · CC0 1.0

BaseCost

Exact module download · Source bundle and reproduction instructions

Increases · constant

payment · input revision 3 · CC0 1.0

Increases

Exact module download · Source bundle and reproduction instructions

InitialFunds · constant

payment · input revision 3 · CC0 1.0

InitialFunds

Exact module download · Source bundle and reproduction instructions

LateUse · constant

payment · input revision 3 · CC0 1.0

LateUse

Exact module download · Source bundle and reproduction instructions

Reductions · constant

payment · input revision 3 · CC0 1.0

Reductions

Exact module download · Source bundle and reproduction instructions

AdmissionMatchesWallet · operator

payment · input revision 3 · CC0 1.0

AdmissionMatchesWallet == Ready => ((ENABLED Pay) <=> available >= Cost)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Cost, Pay, Ready, available

Complete · operator

payment · input revision 3 · CC0 1.0

Complete == /\ pending
            /\ paid' = TRUE
            /\ pending' = FALSE
            /\ UNCHANGED <<available, declined>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: available, declined, paid, pending

Completion · operator

payment · input revision 3 · CC0 1.0

Completion == [](pending => <>~pending)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: pending

Cost · operator

payment · input revision 3 · CC0 1.0

Cost == ModifiedCost(BaseCost, Increases, Reductions)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BaseCost, Increases, Reductions, ModifiedCost

Decline · operator

payment · input revision 3 · CC0 1.0

Decline == /\ Ready
           /\ declined' = TRUE
           /\ UNCHANGED <<available, paid, pending>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Ready, available, declined, paid, pending

DeclineIsUnpaid · operator

payment · input revision 3 · CC0 1.0

DeclineIsUnpaid == declined => (~paid /\ ~pending /\ available = InitialFunds)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InitialFunds, available, declined, paid, pending

EmptyModifiers · operator

payment · input revision 3 · CC0 1.0

EmptyModifiers == <<>>

Exact module download · Source bundle and reproduction instructions

Init · operator

payment · input revision 3 · CC0 1.0

Init == /\ available = InitialFunds
        /\ paid = FALSE
        /\ pending = FALSE
        /\ declined = FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InitialFunds, available, declined, paid, pending

Next · operator

payment · input revision 3 · CC0 1.0

Next == Pay \/ Complete \/ Decline

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Complete, Decline, Pay

NoDoublePayment · operator

payment · input revision 3 · CC0 1.0

NoDoublePayment == paid => ~ENABLED Pay

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Pay, paid

Pay · operator

payment · input revision 3 · CC0 1.0

Pay == /\ Ready
       /\ available >= Cost
       /\ available' = available - Cost
       /\ paid' = ~LateUse
       /\ pending' = TRUE
       /\ UNCHANGED declined

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LateUse, Cost, Ready, available, declined, paid, pending

PaymentIsExact · operator

payment · input revision 3 · CC0 1.0

PaymentIsExact == paid => available = InitialFunds - Cost

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InitialFunds, Cost, available, paid

Ready · operator

payment · input revision 3 · CC0 1.0

Ready == ~paid /\ ~pending /\ ~declined

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: declined, paid, pending

Spec · operator

payment · input revision 3 · CC0 1.0

Spec == Init /\ [][Next]_vars /\ WF_vars(Complete)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Complete, Init, Next, vars

TypeOK · operator

payment · input revision 3 · CC0 1.0

TypeOK == /\ available \in Nat
          /\ paid \in BOOLEAN
          /\ pending \in BOOLEAN
          /\ declined \in BOOLEAN

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: available, declined, paid, pending

UseRecorded · operator

payment · input revision 3 · CC0 1.0

UseRecorded == pending => paid

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: paid, pending

vars · operator

payment · input revision 3 · CC0 1.0

vars == <<available, paid, pending, declined>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: available, declined, paid, pending

available · variable

payment · input revision 3 · CC0 1.0

available

Exact module download · Source bundle and reproduction instructions

declined · variable

payment · input revision 3 · CC0 1.0

declined

Exact module download · Source bundle and reproduction instructions

paid · variable

payment · input revision 3 · CC0 1.0

paid

Exact module download · Source bundle and reproduction instructions

pending · variable

payment · input revision 3 · CC0 1.0

pending

Exact module download · Source bundle and reproduction instructions