Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve the section on authoritative resource algebras #1

Open
jihgfee opened this issue Oct 14, 2022 · 0 comments
Open

Improve the section on authoritative resource algebras #1

jihgfee opened this issue Oct 14, 2022 · 0 comments

Comments

@jihgfee
Copy link
Collaborator

jihgfee commented Oct 14, 2022

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant