[ArquintL]

Closes #48

[ArquintL]

@jcp19 How are the code examples in the book verified? Do I have to do anything such that we would notice if my added example would ever stop verifying?

[Copilot]

Pull request overview

Adds documentation and a companion example file to clarify Gobra’s permission shorthand for shared struct fields, addressing the confusion described in issue #48.

Changes:

• Introduces shared_struct_concise.go with a more concise Scale contract using acc(c).
• Updates addressable.md to mention and demonstrate the acc(c) shorthand via an included snippet.
• Fixes minor punctuation in the Scale description (Scale, → Scale).

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.

File	Description
src/02/shared_struct_concise.go	New example file showing Scale specified with preserves acc(c) for concise “all fields” permissions.
src/02/addressable.md	Documentation update explaining acc(c) shorthand and embedding the new concise snippet.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[felixlinker]

@ArquintL this was actually already explained here: https://github.com/viperproject/gobra-book/blob/main/src%2F02%2Ffractional-permissions.md#L41

[ArquintL]

Ah thanks @felixlinker. It's a bit weird that that paragraph adds more information about shared structs & this shorthand notation despite being in a section on fractional permissions.

[jcp19]

@jcp19 How are the code examples in the book verified? Do I have to do anything such that we would notice if my added example would ever stop verifying?

@ArquintL unfortunately, for now, we don't have a systematic way of testing this. Adding these checks is not just a matter of enabling gobra on all examples, given that not all of them are meant to verify. Ideally, we would be able to reuse the same annotations that we use in the gobra test suite to annotate expected errors, but that requires changing Gobra to accept those annotations in arbitrary files, not just the test suit (might be doable with the support for annotations).

[felixlinker]

Ah thanks @felixlinker. It's a bit weird that that paragraph adds more information about shared structs & this shorthand notation despite being in a section on fractional permissions.

Agreed. Maybe this PR should delete that paragraph and we move it up to shared structs?