diff options
| -rw-r--r-- | requirements/catalogue/req-030.md | 15 | ||||
| -rw-r--r-- | requirements/catalogue/req-036.md | 2 | ||||
| -rw-r--r-- | requirements/catalogue/req-046.md | 2 | ||||
| -rw-r--r-- | requirements/catalogue/req-070.md | 61 | ||||
| -rw-r--r-- | requirements/catalogue/req-071.md | 8 | ||||
| -rw-r--r-- | requirements/catalogue/req-072.md | 5 | ||||
| -rw-r--r-- | requirements/catalogue/req-073.md | 9 |
7 files changed, 97 insertions, 5 deletions
diff --git a/requirements/catalogue/req-030.md b/requirements/catalogue/req-030.md index d211964..4212ec4 100644 --- a/requirements/catalogue/req-030.md +++ b/requirements/catalogue/req-030.md @@ -18,10 +18,17 @@ Inputs: 6. If `is_up_to_date = TRUE`, then return `bucket.balance`. 7. Carry out the procedure, `update_bucket_drips(bucket)`, as described in req-037. -8. Let `transaction_sum` be the sum over the property, `amount`, of all +8. Let `latest_transaction` be the transaction `t` with the most recent + `t.timestamp` such that `t.bucket_id = bucket.id`. +9. Let `transaction_sum` be the sum over the property, `amount`, of all transactions `t` such that `t.bucket_id = bucket.id`. -9. Let `drip_sum` be the sum over the property, `amount`, of all drips `d` such - that `d.bucket_id = bucket.id`. -10. Return `drip_sum - transaction_sum`. +10. Let `latest_drip` be the drip `d` with the most recent `d.timestamp` such + that `d.bucket_id = bucket.id`. +11. Let `drip_sum` be the sum over the property, `amount`, of all drips `d` such + that `d.bucket_id = bucket.id`. +12. Let `balance` be `drip_sum - transaction_sum`. +13. Set `bucket.balance` to `balance`. +14. Set `bucket.balance_cache_key` to + `{latest_drip.id}:{latest_transaction.id}`. Source: req-029 diff --git a/requirements/catalogue/req-036.md b/requirements/catalogue/req-036.md index 723e6e1..bad56e7 100644 --- a/requirements/catalogue/req-036.md +++ b/requirements/catalogue/req-036.md @@ -5,3 +5,5 @@ Given a bucket, `bucket`, if the procedure then the accurate balance of `bucket` is equal to `bucket.balance`. Sources: req-030, req-032 + +Satisfied by: req-070, ass-008 diff --git a/requirements/catalogue/req-046.md b/requirements/catalogue/req-046.md index 493df03..a5f2ea8 100644 --- a/requirements/catalogue/req-046.md +++ b/requirements/catalogue/req-046.md @@ -4,4 +4,4 @@ Schist must record the user's transactions. Source: req-012 -Blocked by: task-007 +Satisfied by: task-001 diff --git a/requirements/catalogue/req-070.md b/requirements/catalogue/req-070.md new file mode 100644 index 0000000..bf155e8 --- /dev/null +++ b/requirements/catalogue/req-070.md @@ -0,0 +1,61 @@ +# req-070 + +Given a bucket, `bucket`, if the procedure +`is_bucket_balance_up_to_date(bucket)` as described in req-035 returns TRUE, +then `bucket.balance` is equal to the difference between the amounts of the +drips into it and the amounts of the transactions out of it. + +Sources: req-036, ass-008 + +Satisfied by: req-030, req-070, req-071, req-072, req-073 + +## Proof + +Grant req-030, req-070, req-071, req-072, req-073. + +Let `bucket` be a bucket, and suppose that +`is_bucket_balance_up_to_date(bucket)` as described in req-035 returns TRUE. + +It follows that: + +- `bucket.balance_cache_key` is of the form `<string>:<string>` +- The first part is the ID of a drip: call it `drip` +- There is no `drip_2` such that `drip_2.timestamp > drip.timestamp` +- The first part is the ID of a transaction: call it `transaction` +- There is no `transaction_2` such that + `transaction_2.timestamp > transaction.timestamp` + +Given req-071, when `bucket.balance_cache_key` was last set to this value, +running `calculate_bucket_balance(bucket)` immediately afterwards would have +left `bucket.balance_cache_key` and `bucket.balance` unchanged, even under the +pretence that `is_bucket_balance_up_to_date(bucket)` returns FALSE. + +Given req-030, running `calculate_bucket_balance(bucket)` at that time under +that pretence would have set `bucket.balance` to the difference between the +amounts of the drips into the bucket and the amounts of the transactions out of +the bucket. + +Since there is no `drip_2` such that `drip_2.bucket_id = bucket.id` and +`drip_2.timestamp > drip.timestamp`, it follows that there are no more drips +into the bucket now than there were then. Symmetrically, it follows that there +are no more transactions out of the bucket now than there were then. + +Given req-072, it follows that there were no more drips into the bucket then +than there are now. + +It follows that there are the same drips into the bucket then and now. It +follows from that, given req-072, that the amounts of the drips into the bucket +are the same now as they were then. + +Given req-073, and the assumption that the time we are considering is the last +time `bucket.balance_cache_key` was set, it follows that no transactions have +been deleted or updated since then, and so it likewise follows that the amounts +of the transactions are the same now as they were then. + +It follows that the difference between the amounts of the drips into it and the +amounts of the transactions out of it has not changed since then. Since that is +ex hypothesi equal to the value of `bucket.balance` which was set at that time, +and since ex hypothesi that is the same value of `bucket.balance` which obtains +now, it follows that `bucket.balance` is equal to the difference between the +amounts of the drips into the bucket and the amounts of the transactions out of +the bucket. QED. diff --git a/requirements/catalogue/req-071.md b/requirements/catalogue/req-071.md new file mode 100644 index 0000000..42f8e2d --- /dev/null +++ b/requirements/catalogue/req-071.md @@ -0,0 +1,8 @@ +# req-071 + +Every time a bucket's `balance` or `balance_cache_key` properties are set or +updated, it must be the case that running `calculate_bucket_balance(bucket)` +under the pretence that `is_bucket_balance_up_to_date(bucket)` returns FALSE +would leave the bucket's `balance` and `balance_cache_key` unchanged. + +Source: req-070 diff --git a/requirements/catalogue/req-072.md b/requirements/catalogue/req-072.md new file mode 100644 index 0000000..f8b8ca3 --- /dev/null +++ b/requirements/catalogue/req-072.md @@ -0,0 +1,5 @@ +# req-072 + +Schist must never delete or update drips. + +Source: req-071 diff --git a/requirements/catalogue/req-073.md b/requirements/catalogue/req-073.md new file mode 100644 index 0000000..b6710de --- /dev/null +++ b/requirements/catalogue/req-073.md @@ -0,0 +1,9 @@ +# req-073 + +Whenever a transaction in Schist is deleted or updated, if the transaction +belongs to a bucket, `bucket`, then Schist must run the procedure, +`calculate_bucket_balance(bucket)`, as described in req-030, under the pretence +that `is_bucket_balance_up_to_date(bucket)` as described in req-035 returns +FALSE. + +Source: req-070 |