The section on authoritative resource algebras could benefit from a slight rewriting.
Some salient points:
- The generally presented rules for the RA are not sufficient for deriving the properties of the fractional use case
- There are some erratas, see below
Known erratas:
- The specifications of Exercise 8.52 do not recover the spatial isCounter predicate in the post-condition.
- Many definition use multiple
∀ x. ∀ y. ∀ z. _ rather than the iterated ∀ x, y, z. _
- The first RA construction uses
m/n for the fragmental piece, but the generalised construction uses a/b
The section on authoritative resource algebras could benefit from a slight rewriting.
Some salient points:
Known erratas:
∀ x. ∀ y. ∀ z. _rather than the iterated∀ x, y, z. _m/nfor the fragmental piece, but the generalised construction usesa/b