Quantified permissions

We speak of quantified permission when access predicates occur within the body of a forall quantifier¹.

This may simplify specifying access to shared arrays, but importantly, it allows us to specify access to a possibly unbounded number of locations ². Whereas arrays have a fixed number of elements, the type of a slice does not contain its length. In the next section on slices, we will use quantified permission to handle their dynamic size. For example, the following precondition specifies write access to all elements of a slice s:

// @ requires forall i int :: {s[i]} 0 <= i && i < len(s) ==> acc(&s[i])
func addToSlice(s []int, n int)

Shared arrays

For shared arrays, using quantified permissions is not compulsory. As an array has a fixed number of elements, we could simply list access to each element. In the following example, we look at how we can concisely specify access to the elements of a shared array.

We mark the array a as shared with /*@@@*/. Now, we may reference it and pass its address to the function reverseInplace. This function reverses the elements by swapping the first element with the last one, the second element with the second last element, and so on, until the entire array is reversed. Note that the loop invariant must also capture which part of the array is still unmodified. This allows the array to be reversed in place, as long as permissions are held to modify its elements. Each element of an array is addressable, and with quantified permissions we can specify access to each with the following assertion, as seen in the contract of reverseInplace:

forall i int :: 0 <= i && i < N ==> acc(&((*p)[i]))

Note that we must dereference the pointer first and that we have access to the location &((*p)[i]), not the value (*p)[i].

const N = 10

// @ preserves forall i int :: 0 <= i && i < N ==> acc(&((*p)[i]))
// @ ensures forall i int :: 0 <= i && i < N ==> (*p)[i] == old((*p)[N-i-1])
func reverseInplace(p *[N]int) {
	// @ invariant 0 <= i && i <= N / 2
	// @ invariant forall i int :: 0 <= i && i < N ==> acc(&((*p)[i]))
	// @ invariant forall j int :: 0 <= j && j < i ==> (*p)[j] == old((*p)[N-j-1]) && (*p)[N-j-1] == old((*p)[j])
	// @ invariant forall j int :: i <= j && j < N-i ==> (*p)[j] == old((*p)[j])
	for i := 0; i < N/2; i += 1 {
		(*p)[i], (*p)[N-i-1] = (*p)[N-i-1], (*p)[i]
	}
}


func client1() {
	a /*@@@*/ := [10]int{0, 1, 2, 3, 4, 5, 6, 7, 8, 9}
	reverseInplace(&a)
	// @ assert a[0] == 9
	// @ assert a[9] == 0
}

We can be more specific and have access to single elements. For example, to increment the first element, only acc(&a[0]) is required.

// @ preserves acc(p)
// @ ensures *p == old(*p) + 1
func inc(p *int) {
	*p = *p + 1
}

func client2() {
	a /*@@@*/ := [10]int{0, 1, 2, 3, 4, 5, 6, 7, 8, 9}
	// @ assert acc(&a[0])
	inc(&a[0])
	// @ assert a[0] == 1
}

For a pointer to an array, we can use the syntactic sugar acc(p) which is short for access to each element (forall i int :: 0 <= i && i < N ==> acc(&((*p)[i]))).

Note that we can still call the function reverse with a shared array. The fact that a variable is shared is local; in this case, only within the scope of client3. reverse returns a new, reversed array. It requires no permissions as the array is copied. But in client3, at least read permission must be held to call reverse(a). If we exhale access to the shared array, we can no longer pass a as an argument.

// @ ensures forall i int :: {a[i]} {r[i]} 0 <= i && i < len(r) ==> r[i] == a[len(a)-i-1]
func reverse(a [N]int) (r [N]int) {
	// @ invariant 0 <= i && i <= len(a)
	// @ invariant forall j int :: 0 <= j && j < i ==> r[j] == a[len(a)-j-1]
	for i := 0; i < len(a); i += 1 {
		r[i] = a[len(a)-i-1]
	}
	return r
}

func client3() {
	a /*@@@*/ := [10]int{0, 1, 2, 3, 4, 5, 6, 7, 8, 9}
	p := &a
	// @ assert acc(p)
	// @ assert forall i int :: 0 <= i && i < N ==> acc(&((*p)[i]))
	r := reverse(a)
	// @ assert r[0] == 9 && r[9] == 0
	// @ assert a[0] == 0 && a[9] == 9
	// @ exhale acc(&a)
	r2 := reverse(a) // error
}

ERROR Reading might fail. 

Permission to a might not suffice.

Injectivity requirement

As a requirement, the mapping between instances of the quantified variable and the receiver expression must be injective. In the example addToSlice, this injective mapping is from i to &s[i].

In the following example, the postcondition of getPointers does not specify that the returned pointers are all distinct. Gobra cannot prove that the mapping is injective and reports an error.

// @ ensures acc(ps[0],1/2) && acc(ps[1],1/2) && acc(ps[2],1/2)
func getPointers() (ps [3]*int) {
	a /*@@@*/, b /*@@@*/, c /*@@@*/ := 0, 1, 2
	return [...]*int{&a, &b, &c}
}
// @ requires forall i int :: {ps[i]} 0 <= i && i < len(ps) ==> acc(ps[i], 1/2)
func consumer(ps [3]*int) { /* ... */ }

func client() {
	ps := getPointers()
	consumer(ps)
}

ERROR Precondition of call consumer(ps) might not hold. 
Quantified resource ps[i] might not be injective.

We can explicitly specify that the pointers are distinct:

// @ ensures acc(ps[0],1/2) && acc(ps[1],1/2) && acc(ps[2],1/2)
// @ ensures forall i, j int :: {ps[i], ps[j]} 0 <= i && i < j && j < len(ps) ==> ps[i] != ps[j]

Alternatively, we can use quantified permissions for the postcondition, which implies the injectivity:

// @ ensures forall i int :: {ps[i]} 0 <= i && i < len(ps) ==> acc(ps[i], 1/2)