Permissions for Shared Struct Shorthand

CONTRIBUTING.md

@@ -19,7 +19,7 @@ This assumes you have [Rust's package manager cargo installed](https://doc.rust-
 
 Install `mdbook` with
 ``` sh
-cargo install mdbook
+cargo install mdbook --locked --version 0.4.40
 ```
 
 For the interactive quizzes we need the `mdbook-quiz` preprocessor and the preprocessor to check all links.

book.toml

@@ -1,7 +1,6 @@
 [book]
 authors = ["Ali Gottschall", "João Pereira"]
 language = "en"
-multilingual = false
 src = "src"
 title = "Practical Program Verification in Go with Gobra (alpha)"
 

src/02/addressable.md

@@ -40,10 +40,10 @@ In this section, we specifically look at _shared structs_.
 An example with _shared arrays_ is shown in a [following section](./quantified-permission.md).
 
 ## Shared structs
-The fields of structs can be addressed individually.
+The fields of structs must be addressed individually.
 For example, access can be specified to the field `x` of a shared struct `c` with `acc(&c.x)`.
 
-In the following example, we use structs representing 2D coordinates and implement a method, `Scale,` to multiply them by a scalar factor.
+In the following example, we use structs representing 2D coordinates and implement a method, `Scale`, to multiply them by a scalar factor.
 ``` go does_not_verify
 {{#include shared_struct.go:Scale}}
 
@@ -69,6 +69,13 @@ We may reference them directly without errors:
 {{#include shared_struct.go:client2}}
 ```
 
+Since one often specifies permissions for all fields of a shared struct `c`, Gobra provides the shorthand `acc(c)`, which is syntactic sugar for `acc(&c.x) && acc(&c.y)` if `x` and `y` are this struct's only fields.
+Thus, `Scale` can be specified more concisely in the following way:
+``` go verifies
+{{#include shared_struct_concise.go:Scale}}
+```
+
+
 ## Shared parameters (`share`)
 It is not possible to mark parameters with `@`, as whether a parameter is shared is local to the function and should not be exposed in its signature.
 Gobra reports errors as we cannot reference the non-shared `c1` and `c2` to call `Scale` on a pointer receiver.

src/02/shared_struct_concise.go

@@ -0,0 +1,43 @@
+package sharedstruct
+
+type Coord struct {
+	x, y int
+}
+
+// ANCHOR: Scale
+// @ preserves acc(c) // changed
+// @ ensures   c.x == old(c.x) * factor
+// @ ensures   c.y == old(c.y) * factor
+func (c *Coord) Scale(factor int) {
+	c.x = c.x * factor
+	c.y = c.y * factor
+}
+
+// ANCHOR_END: Scale
+
+// ANCHOR: client1
+func client1() {
+	c /*@@@*/ := Coord{1, 2}
+	c.Scale(5)
+	// @ assert c == Coord{5, 10}
+}
+
+// ANCHOR_END: client1
+
+// ANCHOR: client2
+func client2() {
+	c := &Coord{1, 2}
+	c.Scale(5)
+	// @ assert *c == Coord{5, 10}
+}
+
+// ANCHOR_END: client2
+
+// ANCHOR: client3
+func client3(c1, c2 Coord) {
+	// @ share c1, c2
+	c1.Scale(5)
+	c2.Scale(-1)
+}
+
+// ANCHOR_END: client3