Overview

This book is an online resource that teaches how to prove the correctness of your programs written in Go against a formal specification. We use the Gobra verifier, and we exemplify it on multiple examples and exercises.

If you find errors or have suggestions, please file an issue here.

If you have any questions about Gobra's features that are not yet addressed in the book, feel free to ask them on Zulip.

Finally, if you are interested in contributing directly to the project, please refer to our guide for contributors.

Basic Specifications

How can we differentiate between a correct and a faulty implementation? Before we can prove that a Go program is correct, we must first make it clear what it means for the program to be correct. In this section, we explain how to do this by associating a contract with each function in the program. The contract for a function has two main components: preconditions and postconditions: Preconditions describe under which conditions a function may be called. Postconditions describe what conditions hold whenever a function returns.

For example, the function Abs should compute the absolute value of a x int32. Mathematically speaking, Abs(x) should return \( |x| \).

// ##(--overflow)

// @ ensures res >= 0 && (res == x || res == -x)
func Abs(x int32) (res int32) {
    if x < 0 {
        return -x
    } else {
        return x
    }
}

This function is annotated with a contract. Contracts may be added to functions via comments that start with the marker // @ or that are in between markers /*@ and @*/ for multi-line annotations, and they must be placed immediately before the function signature. The contract for Abs contains a single postcondition, marked with the ensures keyword, but it may contain more than one. Contracts may also be annotated with multiple preconditions, marked with the requires keyword, as we shall exemplify later. The postcondition res >= 0 && (res == x || res == -x) states that if x is negative, it must be negated, and otherwise the same value must be returned.

To make sure this function is correct, one could test it by writing unit tests, for various inputs. Unfortunately, it is very easy to ignore corner cases when writing tests. There is a subtle bug, which Gobra detects with overflow checking enabled:

ERROR Expression -x might cause integer overflow.

Without this option, Gobra would accept the function Abs.

Go uses two's complement arithmetic, so the minimum signed integer that can be represented with 32 bits is -2147483648, whereas the maximum is 2147483647. Because of this, the computation of the Abs of the minimum integer overflows.

We complete the contract for Abs with a precondition that prevents Abs from being called with MinInt32 as its argument.

// ##(--overflow)
const MinInt32 = -2147483648  // -1<<32

// @ requires x != MinInt32
// @ ensures res >= 0 && (res == x || res == -x)
func Abs(x int32) (res int32)

Gobra only considers function calls that satisfy the precondition. That is why we are able to prove that the postcondition holds by adding this precondition.

It is the programmer's job to specify the functions they write and to provide any annotations that may guide the proof (more on this later). In turn, Gobra checks that all function contracts hold and that the function will never panic (for example, due to a division by zero). If the program fails to verify, Gobra produces helpful error messages that can help to identify the error. These checks happen statically before the program is even compiled. These annotations do not impose any runtime checks, and thus, they do not introduce any changes in the program's behavior or performance. In the next sections, we explain how to prove that a function satisfies its contract and how callers of this function may rely on its contract.

Specifying preconditions with requires clauses

Preconditions are added with the keyword requires before a function declaration. For any reachable call, Gobra checks whether the function's precondition is guaranteed to hold. Since this is enforced, the precondition can be assumed to hold at the beginning of a function. Let us exemplify this with the absolute value example:

const MinInt32 = -2147483648

// @ requires x != MinInt32
// @ ensures res >= 0 && (res == x || res == -x)
func Abs(x int32) (res int32) {
    if x < 0 {
        return -x
    } else {
        return x
    }
}

func client1() {
    v1 := Abs(3)  // v1 == 3
    v2 := Abs(-2) // v2 == 2
    v3 := Abs(MinInt32) // error
}

// @ requires a > 0 && b < 0
func client2(a, b int32) {
    v4 := Abs(a)
    v5 := Abs(b) // error
}

ERROR Precondition of call Abs(MinInt32) might not hold. 
Assertion x != -2147483648 might not hold.
ERROR Precondition of call Abs(b) might not hold. 
Assertion x != MinInt32 might not hold.

The function client1 calls Abs with constant values. For the calls Abs(3) and Abs(-2) the preconditions hold, since clearly 3 != MinInt32 and -2 != MinInt32. This check fails for Abs(MinInt32). The function client2 calls Abs with its arguments constrained by another precondition a > 0 && b < 0. Here the precondition holds for the call Abs(a), since a > 0 implies a != MinInt32. We get another error for Abs(b), as the only information Gobra has about b at this point is b < 0 which does not exclude b != MinInt32.

Please note that the errors are reported at the location of the call since the caller is violating the contract of the function.

Preconditions a > 0 && b < 0 joined by the logical AND can be split into multiple lines. We can write the contract for client2 equivalently as:

// @ requires a > 0
// @ requires b < 0
func client2(a, b int32)

Gobra checks that a function's preconditions hold for every call of that function and reports an error if it cannot prove it.

Gobra assumes the preconditions hold at the beginning of the function's body.

Proof annotation: assert statements

Before we look at postconditions, we introduce our first kind of proof annotation: assert statements. These statements check whether some condition is guaranteed to hold on all program paths that reach it. Because of this, it may be very useful when constructing and debugging proofs, as we shall see throughout this book. As with any other annotations introduced by Gobra, they must occur in comments marked with // @. Once again, notice that Gobra verifies programs before they are even compiled. These checks do not introduce any assertions at runtime, so there is no performance cost to adding these annotations.

The first assertion passes in the following program since it can be inferred from the precondition.

// @ requires a > 0 && b < 0
func client3(a, b int32) {
    // @ assert a > b
    // @ assert b > -10 // error
}

ERROR Assert might fail. 
Assertion b > -10 might not hold.

For an assert statement, Gobra statically checks that the assertion holds and reports an error if it cannot prove it.

Specifying postconditions with ensures clauses

Postconditions are added with the keyword ensures before a function declaration. By convention, they are written after any preconditions. In the contract of the function Abs, we have already seen the postcondition res >= 0 && (res == x || res == -x).

When a function is called, Gobra checks that its preconditions hold at the call site, and if so, the postcondition is assumed. We illustrate this by adding assert statements in the code for client4 that show that the postcondition of Abs holds.

const MinInt32 = -2147483648

// @ requires x != MinInt32
// @ ensures res >= 0 && (res == x || res == -x)
func Abs(x int32) (res int32) {
    // @ assert x != MinInt32
    if x < 0 {
        // @ assert x != MinInt32 && x < 0
        return -x
    } else {
        // @ assert x != MinInt32 && !(x < 0)
        return x
    }
}

func client4() {
    v1 := Abs(3)
    // @ assert v1 >= 0 && (v1 == 3 || v1 == -3)
    // @ assert v1 == 3
    v2 := Abs(-2)
    // @ assert v2 >= 0 && (v2 == -2 || v2 == -(-2))
    // @ assert v2 == 2
}

At the beginning of the function Abs, the precondition holds. Then depending on the branch taken, different constraints hold for x. After the call to Abs, we can assert the postcondition (with the arguments substituted, for example, v2 >= 0 && (v2 == -2 || v2 == -(-2)) implies that v2 == 2 which can also be asserted).

Gobra uses a modular verification approach. Each function is verified independently and all we know about a function at call sites is its contract. This is crucial for scaling verification to large projects.

If we exchange the bodies of the if statement, the function WrongAbs does not satisfy its contract:

const MinInt32 = -2147483648

// @ requires x != MinInt32
// @ ensures res >= 0 && (res == x || res == -x)
func WrongAbs(x int32) (res int32) {
    if x < 0 {
        return x
    } else {
        return -x
    }
}

ERROR Postcondition might not hold. 
Assertion res >= 0 might not hold.

Gobra checks that a function's postconditions hold whenever the function returns and reports an error if it cannot prove it.

Default precondition and postcondition

A requires or ensures clause may be omitted from a contract, or both clauses may be omitted. In such cases, the precondition and postcondition default to true.

func foo() int

is equivalent to

// @ requires true
// @ ensures true
func foo() int

Since true always holds, the precondition true does not restrict when a function can be called. A postcondition true provides no information about the return values.

If no precondition is specified by the user, it defaults to true.

If no postcondition is specified by the user, it defaults to true.

Verifying programs with arrays

In this section, we show how to verify programs that use arrays of fixed size (we will later see how to verify programs with slices, whose length may not be statically known). Programs that access arrays often suffer from subtle bugs such as off-by-one errors, or other kinds of out-of-bounds accesses, that may lead to runtime panics. Gobra prevents these by statically checking that every access to arrays is within bounds.

Go can find out-of-bounds indices for constant values when compiling a program.

package main

import "fmt"

func main() {
	a := [5]int{2, 3, 5, 7, 11}
	fmt.Println(a[-1]) // invalid index (too small)
	fmt.Println(a[1])  // valid index
	fmt.Println(a[10]) // invalid index (too large)
}

./array.go:8:16: invalid argument: index -1 (constant of type int) must not be negative
./array.go:10:16: invalid argument: index 10 out of bounds [0:5]

Unfortunately, the checks that the Go compiler performs may miss simple out-of-bounds errors, as shown in the example below that moves the array access to a different function:

package main

import "fmt"

func main() {
	a := [5]int{2, 3, 5, 7, 11}
	getItem(a, -1)
	getItem(a, 1)
	getItem(a, 10)
}

func getItem(a [5]int, i int) {
	fmt.Println(a[i]) // error
}

Go is memory-safe and checks at runtime whether the index is within bounds:

panic: runtime error: index out of range [-1]

goroutine 1 [running]:
main.getItem(...)
        /home/gobra/array.go:20

Now if we check the program with Gobra we can find the error statically at verification time.

ERROR Assignment might fail. 
Index i into a[i] might be negative.

The indexing operation a[i] implicitly has the precondition requires 0 <= i && i < len(a). By propagating this precondition to the contract of getItem, Gobra accepts the function.

// @ requires 0 <= i && i < len(a)
func getItem(a [5]int, i int) {
	fmt.Println(a[i])
}

Then the calls getItem(a, -1) and getItem(a, 10) will get rejected.

Gobra statically checks that every access to arrays is within bounds.

Quantifiers and Implication

Programs often deal with data structures of unbounded size, such as linked lists and slices, or with data structures that have a fixed size, but which are too large to describe point-wise. As an example, let's assume we want to write a function sort that takes an array arr of type [1000]int and returns a sorted array ¹.

func sort(arr [1000]int) (res [1000]int)

If we want to state that the output of this function is sorted, we could write the postcondition res[0] <= res[1] && res[1] <= .... && res[998] <= res[999]. However, this is extremely impractical to write, debug, and maintain. In this section, we show how we can use quantifiers to concisely capture these properties.

Gobra supports the universal quantifier forall. The existential quantifier exists is available, but its use is discouraged. Additionally, we introduce the logical operator for the implication (==>), which is commonly (but not only) used together with quantifiers.

Universal quantifier forall

To get started, we write an assertion that checks that an array is initialized with zero values:

func client1() {
    var a [1000]int
    // @ assert forall i int :: 0 <= i && i < len(a) ==> a[i] == 0
}

We make use of the forall quantifier to use an arbitrary i of type int. After double colons (::) follows an assertion in which we can use the quantified variable i. Gobra checks that this assertion holds for all instantiations of i and reports an error otherwise.

Here we use an implication (==>) ² to specify that only if i is a valid index (0 <= i && i < len(a)), then the element at this index is zero. All array accesses must be within bounds, as well as in specifications and proof annotations. Without constraining i, the assertion states that a[i] == 0 holds for all possible integers i, which includes amongst others i=-1 and we face the error:

func client2() {
    var a [1000]int
    // @ assert forall i int :: a[i] == 0
}

ERROR Assert might fail. 
Index i into a[i] might be negative.

Returning to the introductory example, let us apply forall to write the postcondition of sort: Another way of specifying that an array is sorted is that for any two array elements, the first element must be smaller than or equal to the second element. So for any integers i and j with i < j it must hold that res[i] <= res[j], again enforcing that the indices i and j are within bounds:

// @ ensures forall i, j int :: 0 <= i && i < j && j < len(res) ==> res[i] <= res[j]
func sort(arr [1000]int) (res [1000]int)

Note that we can quantify i and j at the same time instead of using two forall quantifiers:

// @ requires forall i int :: forall j int ::  0 <= i && i < j && j < len(res) ==> res[i] <= res[j]

Efficient verification with triggers

While a universal quantifier states that an assertion holds for all instantiations of a variable, proofs often require knowing the body of a quantifier for concrete instantiations. Triggers are syntactical patterns that, when matched, trigger Gobra to learn the body of a quantifier with concrete instantiations. They are crucial for ensuring efficient verification.

Trigger expressions are enclosed in curly braces at the beginning of the quantified expression. For example, we add a[i] as a trigger:

forall i int :: { a[i] } 0 <= i && i < len(a) ==> a[i] == 0`

Now when a[3] matches a[i], for example in assert a[3] == 0, Gobra learns the body of the quantifier where i is instantiated with 3:

0 <= 3 && 3 < len(a) ==> a[3] == 0

Existential quantifier exists

For the existential quantifier, Gobra checks that the assertion holds for at least one instantiation of the quantified variable.

For completeness, we still show an example: The function Contains returns whether the value target is contained in the input array. We can specify with an implication that if target is found there must exist an index idx with arr[idx] == target:

// @ ensures found ==> exists idx int :: 0 <= idx && idx < len(arr) && arr[idx] == target
func Contains(arr [10]int, target int) (found bool) {
    for i := range arr {
        if arr[i] == target {
            return true
        }
    }
    return false
}

func client3() {
    arr := [10]int{0, 1, 2, 3, 4, 5, 6, 7, 8, 9}
    found := Contains(arr, 10)
    // @ assert !found
    found4 := Contains(arr, 4)
}

Note we can only assert that 10 is contained since there does not exist a idx with arr[idx] = 10, indirectly !found must hold. To fully capture the intended behavior of Contains, the contract should include a postcondition for the case where target is not found:

// @ ensures !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target

So far, we cannot prove this without adding additional proof annotations.

Loops

Reasoning with loops introduces a challenge for verification. Loops may execute an unbounded number of iterations. As is typical in program verification, we reason about loops through loop invariants, i.e., assertions that describe properties that hold for all iterations of the loop.

Using the example of a binary search, we showcase how we can gradually build up the invariant until we are able to verify the function.

We will also introduce the verification of loops with range clauses.

Termination of loops will be discussed in a following section.

Loop Invariants

A loop invariant is an assertion that is preserved by the loop across iterations.

Gobra checks that the invariant holds

1. before the first iteration after performing the initialization statement
2. after every iteration

We can specify it with the keyword invariant before a loop.

// @ invariant ASSERTION
for condition { // ... }

Similarly to requires and ensures, you can split an invariant on multiple lines.

Finding loop invariants, in general, can be quite hard. In the general case, there is no procedure to figure out which invariants are needed to verify a program against a specification. Nonetheless, it does get much easier the more you do it, and we hope to show it on a few examples step-by-step.

As a first example, the function LinearSearch searches an array for the value target. If target is found, idx shall be its index. Otherwise, no element of the array shall be equal to target. This function bears similarity to Contains from the section on quantifiers, with the difference that we additionally return the index, which allows us to avoid an existential quantifier. Here, we will be able to prove the contract for the case found ==> .... as well by providing appropriate loop invariants.

package linearsearch

// @ ensures found ==> 0 <= idx && idx < len(arr) && arr[idx] == target
// @ ensures !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target
func LinearSearch(arr [10]int, target int) (idx int, found bool) {
	// @ invariant 0 <= i && i <= len(arr)
	// @ invariant forall j int :: 0 <= j && j < i ==> arr[j] != target
	for i := 0; i < len(arr); i += 1 {
		if arr[i] == target {
			return i, true
		}
	}
	return -1, false
}

func client() {
	arr := [10]int{0, 1, 2, 3, 4, 5, 6, 7, 8, 9}
	i10, found := LinearSearch(arr, 10)
	// @ assert !found
	// @ assert forall i int :: 0 <= i && i < len(arr) ==> arr[i] != 10
	// @ assert arr[4] == 4
	i4, found4 := LinearSearch(arr, 4)
	// @ assert found4
	// @ assert arr[i4] == 4
}

Gobra cannot track all possible values for the loop variable i over all iterations and we must help by specifying bounds for i with:

invariant 0 <= i && i <= len(arr)

Without this invariant, Gobra reports the error:

ERROR Loop invariant is not well-formed. 
Index j into arr[j] might exceed sequence length.

Let us check manually whether this invariant holds:

1. We initialize i := 0, so the invariant holds before the first loop iteration.
2. The loop guard is i < len(arr). After the statement i += 1, the condition i <= len(arr) holds. From the invariant, we know that 0 <= i held before this iteration. Therefore, after incrementing, 1 <= i holds. Combining these observations, we conclude that 0 <= i && i <= len(arr) holds after an arbitrary iteration, preserving the invariant.

invariant forall j int :: 0 <= j && j < i ==> arr[j] != target

Without this second invariant, Gobra cannot prove a postcondition:

ERROR Postcondition might not hold. 
Assertion !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target might not hold.
!found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target

This invariant captures the "work" the loop has done so far: all elements with index smaller than i have been checked and are not equal to target.

When the loop condition i < len(arr) fails, i >= len(arr) holds. The first invariant states that i <= len(arr). Therefore i == len(arr) and forall i int :: 0 <= i && i < len(arr) ==> arr[i] != target holds.

Failing to establish an invariant

When we change the first invariant to use 1 <= i instead of 0 <= i, this invariant does not hold before the first iteration:

func NotEstablished(arr [N]int, target int) (idx int, found bool) {
	// @ invariant 1 <= i && i <= len(arr)
	for i := 0; i < len(arr); i += 1 {
		if arr[i] == target {
			return i, true
		}
	}
	return -1, false
}

ERROR Loop invariant might not be established. 
Assertion 1 <= i might not hold.

Failing to preserve an invariant

When we change the first invariant to use i < len(arr) instead of i <= len(arr), this invariant does not hold after every iteration. After the last iteration i==len(arr) holds and this invariant is not preserved.

func NotPreserved(arr [N]int, target int) (idx int, found bool) {
	// @ invariant 0 <= i && i < len(arr)
	for i := 0; i < len(arr); i += 1 {
		if arr[i] == target {
			return i, true
		}
	}
	return -1, false
}

ERROR Loop invariant might not be preserved. 
Assertion i < len(arr) might not hold.

Gobra checks that a loop invariant holds

1. before the first iteration after performing the initialization statement
2. after every iteration

Binary Search

We will follow along with the example of the function BinarySearchArr(arr [N]int, target int) (idx int, found bool), adapted from Go's BinarySearch for slices. Here we use arrays of integers instead of generic slices: The contract we write formalizes the docstring:

// BinarySearch searches for target in a sorted slice and returns the earliest
// position where target is found, or the position where target would appear
// in the sort order; it also returns a bool saying whether the target is
// really found in the slice. The slice must be sorted in increasing order.
func BinarySearch[S ~[]E, E cmp.Ordered](x S, target E) (int, bool)

The following snippet shows the expected results for a test cases:

func main() {
	arr := [7]int{0, 1, 1, 2, 3, 5, 8}
	fmt.Println(BinarySearchArr(arr, 2))   // 3 true
	fmt.Println(BinarySearchArr(arr, 4))   // 5 false
	fmt.Println(BinarySearchArr(arr, -1))  // 0 false
	fmt.Println(BinarySearchArr(arr, 10))  // 7 false
}

Our approach is to gradually add specifications and fix errors along the way. To see the final code only, you can skip to the end of this section.

Let us begin by writing a first contract. First, we must require the array arr to be sorted. We have already discussed how to specify this:

// @ requires forall i, j int :: {arr[i], arr[j]} 0 <= i && i < j && j < len(arr) ==> arr[i] <= arr[j]

If BinarySearchArr returns not found, target must not be an element of arr, or equivalently, all elements of arr are not equal to target:

// @ ensures !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target

For the case where target is found, idx gives its position:

// @ ensures found ==> 0 <= idx && idx < len(arr) && arr[idx] == target

This contract does not yet capture that idx must be the first index where target is found or otherwise the position where target would appear in the sort order.

Here is the first implementation of BinarySearchArr. The elements with an index between low and high denote the parts of the array that remain to be searched for target. We must add several loop invariants until this function satisfies its contract.

const N = 1000

// @ requires forall i, j int :: {arr[i], arr[j]} 0 <= i && i < j && j < N ==> arr[i] <= arr[j]
// @ ensures !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target
// @ ensures found ==> 0 <= idx && idx < len(arr) && arr[idx] == target
func BinarySearchArr(arr [N]int, target int) (idx int, found bool) {
	low := 0
	high := len(arr)
	mid := 0
	for low < high {
		mid = (low + high) / 2
		if arr[mid] < target {
			low = mid + 1
		} else {
			high = mid
		}
	}
	return low, low < len(arr) && arr[low] == target
}

ERROR Conditional statement might fail. 
Index mid into arr[mid] might be negative.

The variable mid is computed as the average of low and high. After comparing target with the element arr[mid], we can half the search range: If target is larger, we search in the upper half between mid+1 and high. Otherwise, we search in the lower half between low and mid. For this, we need the invariant that mid remains a valid index for arr:

	// @ invariant 0 <= mid && mid < len(arr)

Let us check whether this invariant works:

1. Before the first iteration mid is initialized to 0. Therefore, 0 <= mid && mid < N trivially holds.
2. For an arbitrary iteration, assume that the invariant 0 <= mid && mid < N held before this iteration. Now we need to show that after updating mid = (low + high) / 2, the invariant is still holds (since the rest of the body does not influence mid). However, this cannot be proven without establishing bounds for low and high.

We know that low and high stay between 0 and len(arr), and low should be smaller than high, right?

	// @ invariant 0 <= low && low < high && high <= len(arr)
	// @ invariant 0 <= mid && mid < len(arr)

ERROR Loop invariant might not be preserved. 
Assertion low < high might not hold.

The condition low < high holds before the first iteration and for every iteration except the last. However, an invariant must hold after every iteration, including the last. To address this, we weaken the condition low < high to low <= high.

Note that after exiting the loop, the loop condition gives !(low < high), while the invariant ensures low <= high. Together, these imply low == high.

Our next challenge is to find invariants that describe which parts of the array have already been searched and are guaranteed to not contain target. By the final iteration, these invariants, combined with low == high, should be sufficient to prove the postcondition. Currently we get the error:

ERROR Postcondition might not hold. 
Assertion !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target might not hold.

To help us find the invariant, let us exemplify the execution of binary search with concrete arguments BinarySearchArr([7]int{0, 1, 1, 2, 3, 5, 8}, 4). The following expressions are evaluated at the beginning of the loop and once after the loop:

We observe a pattern: the slice arr[low:high] denotes the part of the array we still have to search for. All elements in the prefix arr[:low] are smaller than target, and all elements in the suffix arr[high:] are greater than or equal to target. Translating this into invariants gives, we have:

	// @ invariant forall i int :: {arr[i]} 0 <= i && i < low ==> arr[i] < target
	// @ invariant forall j int :: {arr[j]} high <= j && j < len(arr) ==>  target <= arr[j]

Since the array is still known to be sorted, we can simplify this further by relating target to the elements arr[low-1] and arr[high], while ensuring that the indices remain within bounds.

	// @ invariant low > 0 ==> arr[low-1] < target
	// @ invariant high < len(arr) ==>  target <= arr[high]

When exiting the loop, we know that low == high. If target is contained in arr, it must be located at index low, which we check for with arr[low] == target. By combining all invariants, the postcondition can be proven now. However, clients still fail to assert some desired properties.

func InitialClient() {
	arr := [7]int{0, 1, 1, 2, 3, 5, 8}
	i1, found1 := BinarySearchArr(arr, 1)
	i2, found2 := BinarySearchArr(arr, 2)
	i4, found4 := BinarySearchArr(arr, 4)
	// @ assert found1  // Assert might fail.
	// @ assert i1 == 1 // Assert might fail.
	// @ assert found2  // Assert might fail.
	// @ assert i4 == 5 // Assert might fail.
	// @ assert !found4
}

While we know for certain that 4 is not contained, the current postcondition does not provide any information about the index in other cases. For example, it does not guarantee that the position of the first occurrence of duplicate 1s will be returned. We need to include in the contract that idx is the position where target would appear in the sort order.

// @ ensures 0 <= idx && idx <= len(arr)
// @ ensures idx > 0 ==> arr[idx-1] < target
// @ ensures idx < len(arr) ==>  target <= arr[idx]

This stronger contract still follows from the loop invariants. Let us take a step back and take a look at the contract which has grown quite large:

// @ requires forall i, j int :: {arr[i], arr[j]} 0 <= i && i < j && j < len(arr) ==> arr[i] <= arr[j]
// @ ensures 0 <= idx && idx <= len(arr)
// @ ensures idx > 0 ==> arr[idx-1] < target
// @ ensures idx < len(arr) ==> target <= arr[idx]
// @ ensures !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target
// @ ensures found ==> 0 <= idx < len(arr) && arr[idx] == target
func BinarySearchArr(arr [N]int, target int) (idx int, found bool)

We can simplify the cases with !found and found to

// @ found == (idx < len(arr) && arr[idx] == target)

The previous postcondition, found ==> 0 <= idx < len(arr) && arr[idx] == target, is directly covered by the new postcondition, combined with 0 <= idx && idx <= len(arr). The other postcondition, !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target, is also covered. For !found, one of the following must hold:

1. idx >= len(arr). In this case, from idx > 0 ==> arr[idx - 1] < target and idx <= len(arr), it follows that arr[len(arr) - 1] < target. This implies that target is not contained in the array, as the array is sorted.

2. idx < len(arr) and arr[idx] != target. From the postcondition idx < len(arr) ==> target <= arr[idx], we can infer that arr[idx] > target. Since the array is sorted, target is not contained in arr[idx:]. Additionally, the postcondition idx > 0 ==> arr[idx - 1] < target ensures that target is not contained in arr[:idx].

The full example can be found below.

Full Example

package binarysearcharr

const N = 7

func FinalClient() {
	arr := [7]int{0, 1, 1, 2, 3, 5, 8}
	i1, found1 := BinarySearchArr(arr, 1)
	// @ assert found1 && arr[i1] == 1 && i1 == 1
	i2, found2 := BinarySearchArr(arr, 2)
	// @ assert found2 && arr[i2] == 2 && i2 == 3
	i4, found4 := BinarySearchArr(arr, 4)
	// @ assert !found4 && i4 == 5
	i10, found10 := BinarySearchArr(arr, 10)
	// @ assert !found10 && i10 == len(arr)
}

// @ requires forall i, j int :: {arr[i], arr[j]} 0 <= i && i < j && j < len(arr) ==> arr[i] <= arr[j]
// @ ensures 0 <= idx && idx <= len(arr)
// @ ensures idx > 0 ==> arr[idx-1] < target
// @ ensures idx < len(arr) ==> target <= arr[idx]
// @ ensures found == (idx < len(arr) && arr[idx] == target)
func BinarySearchArr(arr [N]int, target int) (idx int, found bool) {
	low := 0
	high := len(arr)
	mid := 0
	// @ invariant 0 <= low && low <= high && high <= len(arr)
	// @ invariant 0 <= mid && mid < len(arr)
	// @ invariant low > 0 ==> arr[low-1] < target
	// @ invariant high < len(arr) ==> target <= arr[high]
	for low < high {
		// fmt.Println(low, high, arr[:low], arr[low:high], arr[high:])
		mid = (low + high) / 2
		if arr[mid] < target {
			low = mid + 1
		} else {
			high = mid
		}
	}
	// fmt.Println(low, high, arr[:low], arr[low:high], arr[high:])
	return low, low < len(arr) && arr[low] == target
}

Range Loops

Besides traditional for loops, Go supports iterating over data structures with for-range loops. In this section, we consider range clauses for arrays. We show how to reason about for-range loops that iterate over slices and maps in their corresponding sections. These data structures pose additional challenges, as they may be concurrently accessed, and thus, we need to employ permissions when reasoning about them. Gobra does not support range clauses for integers, strings, and functions.

Here we refactor the LinearSearch example from the section on loop invariants to use a for-range loop. The contract is left unchanged, but Gobra reports an error:

const N = 10

// @ ensures found ==> 0 <= idx && idx < len(arr) && arr[idx] == target
// @ ensures !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target
func LinearSearch(arr [N]int, target int) (idx int, found bool) {
	// @ invariant 0 <= i && i <= len(arr)
	// @ invariant forall j int :: 0 <= j && j < i ==> arr[j] != target
	for i, a := range arr {
		if a == target {
			return i, true
		}
	}
	return -1, false
}

ERROR Postcondition might not hold. 
Assertion !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target might not hold.

We have come across the pattern where the negation of the loop condition, combined with the invariant, often implies the postcondition. In a standard for loop, we can deduce that i == len(arr) holds after the final iteration. In the range version, however, i equals len(arr) - 1 during the last iteration. Since the range version has no explicit loop condition, Gobra only knows that 0 <= i && i < len(arr) holds during the after iteration, which is insufficient to prove the postcondition.

Helper loop variable from a with clause

We can specify an additional loop variable i0 defined using with i0 after a range clause. The invariant 0 <= i0 && i0 <= len(arr) holds, as does i0 < len(arr) ==> i == i0. Additionally, i0 will be equal to len(arr) at the end of the loop. Thus, if we replace i with i0 in the second invariant, Gobra can verify the postcondition. The invariant 0 <= i && i < len(arr) can be removed, as it is implicitly understood by Gobra. Our final verifying version is:

package main

const N = 10

// @ ensures found ==> 0 <= idx && idx < len(arr) && arr[idx] == target
// @ ensures !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target
func LinearSearchRange(arr [N]int, target int) (idx int, found bool) {
	// @ invariant forall j int :: 0 <= j && j < i0 ==> arr[j] != target
	for i := range arr /*@ with i0 @*/ {  // <--- added with
		if arr[i] == target {
			return i, true
		}
	}
	return -1, false
}

func client() {
	arr := [10]int{0, 1, 2, 3, 4, 5, 6, 7, 8, 9}
	i10, found := LinearSearchRange(arr, 10)
	// @ assert !found
	// @ assert forall i int :: 0 <= i && i < len(arr) ==> arr[i] != 10
	// @ assert arr[4] == 4
	i4, found4 := LinearSearchRange(arr, 4)
	// @ assert found4
	// @ assert arr[i4] == 4
}

Overflow Checking

Usage

By default, Gobra performs no overflow checking. On the command line, you can enable overflow checking with the --overflow or -o flag. The size of int is implementation-specific in Go and either 32 or 64 bits. For overflow checking, Gobra assumes that ints have 64 bits by default. We may change the behavior of Gobra to consider ints with 32 bits by passing the --int32 flag. In a file, we can enable overflow checking by adding the following line:

// ##(--overflow)

Overflow in binary search

If we check our binary search program for large arrays with overflow checking enabled, Gobra detects a potential overflow.

package binarysearch

// ##(--overflow)

const MaxInt64 = 1<<63 - 1
const N = MaxInt64

// @ requires forall i, j int :: {arr[i], arr[j]} 0 <= i && i < j && j < len(arr) ==> arr[i] <= arr[j]
// @ ensures 0 <= idx && idx <= len(arr)
// @ ensures idx > 0 ==> arr[idx-1] < target
// @ ensures idx < len(arr) ==> target <= arr[idx]
// @ ensures found == (idx < len(arr) && arr[idx] == target)
func BinarySearchOverflow(arr [N]int, target int) (idx int, found bool) {
	low := 0
	high := len(arr)
	mid := 0
	// @ invariant 0 <= low && low <= high && high <= len(arr)
	// @ invariant 0 <= mid && mid < len(arr)
	// @ invariant low > 0 ==> arr[low-1] < target
	// @ invariant high < len(arr) ==> target <= arr[high]
	for low < high {
		mid = (low + high) / 2  // <--- problematic expression
		if arr[mid] < target {
			low = mid + 1
		} else {
			high = mid
		}
	}
	if low < len(arr) {
	 	return low, arr[low] == target
	} else {
	 	return low, false
	}
}

ERROR Expression may cause integer overflow.
Expression (low + high) / 2 might cause integer overflow.

For example, for low = N/2 and high = N, the sum low + high cannot be represented by an int and the result will be negative. The solution is to replace the offending statement mid = (low + high) / 2 with:

mid = (high-low)/2 + low

The subtraction does not overflow since high >= low and low >= 0 holds. After this change, Gobra reports no errors.

If we tweak the const N that denotes the array length to 1<<31 which is larger than MaxInt32, we get an error when checking with --int32 --overflow. Verification succeeds when only check with --overflow.

A similar bug was present in Java's standard library (Read All About It: Nearly All Binary Searches and Mergesorts are Broken). This highlights why heavily used code such as packages from the standard library should be verified.

Termination

Having discussed loops, the next thing to address is termination. Here we look at the termination of loops and recursive functions. In general, proving termination is undecidable. However, for functions we write in practice, it is usually not hard to show termination. By default, Gobra checks for partial correctness, i.e., correctness with respect to specifications if the function terminates. For total correctness, both termination and correctness with respect to specifications must be proven. To prove termination, Gobra uses termination measures, i.e., expressions that are strictly decreasing and bounded from below.

Partial correctness

Let us explore the concept of partial correctness further. The function infiniteZero contains an infinite loop, so it will not terminate. It is still partially correct with respect to its contract since the postcondition false must only be proven to hold when it returns, which it does not.

ensures false
func infiniteZero() res {
    for {}
    return 0
}

func main() {
    r := infiniteZero()
    assert r == 1
}

When the function main is verified, it is unknown whether infiniteZero terminates. However, the contract guarantees that when infiniteZero returns, its postcondition holds. Assuming it terminates, we can assert an arbitrary property, such as r == 1. This is fine since, if we run the program, this statement will never be reached.

Specifying termination measures with decreases

We can instruct Gobra to check for termination by adding the decreases keyword to the specification of a function or a loop. It must come right before the function/loop after any preconditions/postconditions/invariants. Sometimes, this suffices and a termination measure can be automatically inferred. For example, for simple functions like Abs that terminate immediately:

decreases
func Abs(x int) (res int) {
    if x < 0 {
       return -x 
    } else {
       return x
    }
}

In other cases, we need to provide a termination measure. A termination measure must be

• lower-bounded
• decrease

For functions, it must decrease for every recursive invocation. Respectively for loops, it must decrease for every iteration.

What it means to be lower-bounded and to be decreasing is defined by Gobra for different types. For example, integers i, j int are lower-bounded if i >= 0 and decreasing if i < j.

Termination of loops

A common case is that we iterate over an array with an increasing loop variable i, as seen in the function LinearSearch. We can easily construct a termination measure that decreases instead by subtracting i from the array's length.

// @ ensures found ==> 0 <= idx && idx < len(arr) && arr[idx] == target
// @ ensures !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i] != target
// @ decreases
func LinearSearch(arr [10]int, target int) (idx int, found bool) {
    // @ invariant 0 <= i && i <= len(arr)
    // @ invariant forall j int :: 0 <= j && j < i ==> arr[j] != target
    // @ decreases len(arr) - i
    for i := 0; i < len(arr); i += 1 {
        if arr[i] == target {
            return i, true
    }
    }
   return -1, false
}

// @ decreases
func client() {
    arr := [10]int{0, 1, 2, 3, 4, 5, 6, 7, 8, 9}
    i10, found := LinearSearch(arr, 10)
    // @ assert !found
    // @ assert forall i int :: 0 <= i && i < len(arr) ==> arr[i] != 10
    // @ assert arr[4] == 4
    i4, found4 := LinearSearch(arr, 4)
    // @ assert found4
    // @ assert arr[i4] == 4
}

We can also prove that client terminates since besides the calls to LinearSearch, which terminate, there is no diverging control flow. If we do not specify a termination measure decreases len(arr) - i for the loop, Gobra reports the error:

ERROR Function might not terminate. 
Required termination condition might not hold.

Termination of recursive functions

The function fibonacci recursively computes the n'th iterate of the Fibonacci sequence. As a termination measure, the parameter n is suitable since we recursively call fibonacci with smaller arguments and n is bounded from below.

// @ requires n >= 0
// @ decreases n
func fibonacci(n int) int {
    if n <= 1 {
        return n
    } else {
        return fibonacci(n-1) + fibonacci(n-2)
    }
}

Verification fails, if we mistype buggynacci(n-0) instead of buggynacci(n-1).

// @ requires n >= 0
// @ decreases n
func buggynacci(n int) int {
    if n == 0 || n == 1 {
        return n
    } else {
        return buggynacci(n-0) + buggynacci(n-2)
    }
}

ERROR Function might not terminate. 
Termination measure might not decrease or might not be bounded.

Assuming termination with decreaes _

If we annotate a function or method with decreases _, termination is assumed and not checked.

This can be dangerous. With the termination measure _ we can assume that buggynacci terminates. Then the following program verifies, where we want to prove that the client code terminates. In practice, buggynacci would never return and doSomethingVeryImportant would never be called.

//@ decreases
//@ func doSomethingVeryImportant()

// @ requires n >= 0
// @ decreases _
func buggynacci(n int) int {
    if n == 0 || n == 1 {
        return n
    } else {
        return buggynacci(n-0) + buggynacci(n-2)
    }
}

//@ decreases
func client() {
    x := buggynacci(n) 
    doSomethingVeryImportant()
}

The use of the wildcard measure can be justified when termination is proven by other means, for example leveraging a different tool. Another use case is gradual verification where it can be useful to assume termination of functions in a codebase, that have not yet been verified.

Termination of binary search

Let us look again at the binary search example. This time we introduce an implementation error: low is updated to low = mid instead of low = mid + 1. BinarySearchArr could loop forever, for example, with BinarySearchArr([7]int{0, 1, 1, 2, 3, 5, 8}, 8). Without decreases, the function would still verify since only partial correctness is checked.

// @ requires forall i, j int :: {arr[i], arr[j]} 0 <= i && i < j && j < len(arr) ==> arr[i] <= arr[j]
// @ ensures 0 <= idx && idx <= len(arr)
// @ ensures idx > 0 ==> arr[idx-1] < target
// @ ensures idx < len(arr) ==> target <= arr[idx]
// @ ensures found == (idx < len(arr) && arr[idx] == target)
// @ decreases  // <--- added for termination checking
func BinarySearchArr(arr [N]int, target int) (idx int, found bool) {
    low := 0
    high := len(arr)
    mid := 0
    // @ invariant 0 <= low && low <= high && high <= len(arr)
    // @ invariant 0 <= mid && mid < len(arr)
    // @ invariant low > 0 ==> arr[low-1] < target
    // @ invariant high < len(arr) ==> target <= arr[high]
    // @ decreases high - low   // <-- added for termination checking
    for low < high {
        mid = (low + high) / 2
        if arr[mid] < target {
            low = mid // <--- Implementation Error, should be low=mid+1
        } else {
            high = mid
        }
    }
    return low, low < len(arr) && arr[low] == target
}

ERROR Function might not terminate. 
Required termination condition might not hold.

We might be tempted to try decreases high or decreases len(arr)-low as termination measures for the loop. However, this is not enough since the termination measure must decrease in every iteration. In iterations where we update low, high does not decrease, and vice versa. The solution is to combine the two as decreases high - low. This measure coincides with the length of the subarray that has not been searched yet. If we change back to low=mid+1, the program verifies again.

Decreases tuple

Sometimes, it might be hard to find a single expression that decreases. In general, one can specify a list of expressions with decreases E1, E2, ..., EN.

A tuple termination measure decreases based on the lexicographical order of the tuple elements.

For BinarySearchArr we used decreases high - low. Alternatively, we could use:

decreases high, len(arr) - low

TODO Conditional termination with if clauses

TODO Mutual recursive functions

Ghost code

Often, it is useful to introduce ghost state and ghost code, i.e., additional state and code that is used for specification and verification purposes, but which is not meant to be compiled and executed. Ghost code cannot change the visible behavior of a program, i.e., it cannot assign to non-ghost variables or cause the program to not terminate.

Ghost code is considered by Gobra but it is ignored during compilation. When writing Gobra annotations in Go source files, the syntax // @ makes it clear that the line is treated as a comment by Go and is not included in the program.

Ghost parameters

Consider the function Max that returns the maximum element of an array, with the signature:

// @ ensures forall i int :: 0 <= i && i < len(arr) ==> arr[i] <= res
// @ ensures exists i int :: 0 <= i && i < len(arr) ==> arr[i] == res
func Max(arr [10]int) (res int)

Verifying this function would be challenging because of the existential quantifier. Additionally, the postcondition gives clients only the maximal value.

With a ghost out parameter idx, we can return the index of the maximal value. The updated contract specifies, that the maximal value is at index idx. We update idx with a ghost statement to maintain the invariant that it is the index of the maximal value in the prefix of the array already iterated over. As Max has two out parameters now, clients must assign the ghost return value to a ghost location.

const N = 10

// @ ensures forall i int :: 0 <= i && i < len(arr) ==> arr[i] <= res
// @ ensures 0 <= idx && idx < len(arr) && arr[idx] == res
func Max(arr [N]int) (res int /*@ , ghost idx int @*/) {
    res = arr[0]
    // @ invariant 0 <= i0 && i0 <= N
    // @ invariant forall j int :: 0 <= j && j < i0 ==> arr[j] <= res
    // @ invariant 0 <= idx && idx < N && arr[idx] == res
    for i, a := range arr /*@ with i0 @*/ {
        if a > res {
            res = a
            // @ ghost idx = i
        }
    }
    return res /*@ , idx @*/
}

func client() {
    arr := [10]int{0, 2, 4, 8, 10, 1, 3, 5, 7, 9}
    // @ assert arr[4] == 10
    // @ ghost var idx int
    m, /*@ idx @*/ := Max(arr)
    // @ assert arr[idx] == m
    // @ assert m == 10
}

Ghost erasure property

Recall that ghost code cannot change the visible behavior of a program. Hence, ghost code cannot modify non-ghost locations. For example, the ghost statement x = 1 causes an error since x is a normal variable:

    var x int
    // @ ghost x = 1
    // ...

ERROR ghost error: only ghost locations can be assigned to in ghost code

To make a statement ghost, add ghost before it. Although not all statements can appear in ghost code. For example, there is no ghost return statement, because it can change the visible behavior of a program:

func loop() {
    // @ ghost return
    for {}
}

ERROR ghost error: expected ghostifiable statement

Termination of ghost functions

Ghost functions must be proven to terminate. Calling a non-terminating ghost function could change the visible behavior of a program. For example, the function boo does not terminate with ghost code but returns immediately without ghost code..

/*@
ghost
func inf() {
    for {}
}
@*/

// @ decreases
func boo() int {
    // @ ghost inf()
    return 42
}

ERROR loop occurring in ghost context does not have a termination measure
    for {}
 ^

More ghost entities

In general, Gobra allows marking the following entities as ghost:

• in and out parameters of functions and methods
• functions and methods where all in- and out-parameters are implicitly ghost
• variables ghost var x int = 42
• statements

We will continue using ghost code in the following chapters.

Pure functions

A function that is deterministic and has no side effects can be marked as pure and may be used in specifications and proof annotations.

If we try to call a normal Go function Cube in an assert statement, Gobra reports errors:

package main

func Cube(x int) int {
    return x * x * x
}

func client() {
    // @ assert 8 == Cube(2)
}

ERROR /tmp/playground.go:8:9:error: expected pure expression, but got '8 ==  Cube(3)'
    assert 8 == Cube(3)
        ^
ERROR /tmp/playground.go:8:14:error: ghost error: Found call to non-ghost impure function in ghost code
    assert 8 == Cube(3)
             ^

Let us mark the function Cube as pure, and also with decreases, since a termination measure is a requirement for a pure function. Gobra enforces the syntactic requirement that the body of pure functions must be a single return with a pure expression, which is satisfied in this case.

// @ pure
// @ decreases
func Cube(x int) int {
    return x * x * x
}

// @ requires n >= 0
func client(n int) {
    // @ assert 8 == Cube(2)
    // @ assert Cube(2) >= 8 && Cube(2) <= 8
    r := Cube(2)
// @ assert Cube(n) >= 0
}

Note that we may call pure functions in normal (non-ghost) code, unlike ghost functions. The assertion passes, even without a postcondition. Unlike normal functions, Gobra may peek inside the body of a function. For example, Cube(n) can be treated as n * n * n

Specifying functional correctness with pure functions

We define a pure function fibonacci as a mathematical reference implementation, following the recursive definition of the Fibonacci sequence. While recursion is not idiomatic in Go, recursion is often used for specifications. In the end, our goal is to verify the functional correctness of an iterative implementation that can be defined in terms of the pure function.

// @ requires n >= 0
// @ ensures res == fibonacci(n)
func fibIterative(n int) (res int) {
	a, b := 0, 1
	for i := 0; i < n; i++ {
		a, b = b, a + b
	}
	return a
}

Syntactic restriction

Gobra enforces the syntactic restriction that the body of pure functions must be a single return with a pure expression. Hence, we are unable to define fibonacci with an if statement:

// @ requires n >= 0
// @ pure
// @ decreases n
func fibonacci(n int) (res int) {
    if n <= 1 {
        return n
    } else {
        return fibonacci(n-1) + fibonacci(n-2)
    }
}

ERROR /tmp/playground.go:17:33:error: For now, the body of a pure block is expected to be a single return with a pure expression, got Vector(if n <= 1 {
  return n
} else {
  return  fibonacci(n - 1) +  fibonacci(n - 2)
}
) instead
func fibonacci(n int) (res int) {
                                ^

Instead, we can resort to the conditional expression cond ? e1 : e2, which evaluates to e1 if cond holds, and to e2 otherwise:

// @ requires n >= 0
// @ pure
// @ decreases n
func fibonacci(n int) (res int) {
    return n <= 1 ? n : fibonacci(n-1) + fibonacci(n-2)
}

Error at: </home/gobra/fibonacci.go:6:24> ghost error: ghost cannot be assigned to non-ghost
func fibonacci(n int) (res int) {
                       ^

An error is reported since the conditional expression is a ghost operation. The error can be avoided by declaring the out parameter as (ghost res int), but we prefer to mark the entire function ghost, as this function is not valid Go code.

/*@
ghost
requires n >= 0
decreases n
pure
func fibonacci(n int) (res int) {
    return n <= 1 ? n : fibonacci(n-1) + fibonacci(n-2)
}
@*/

Pure functions are transparent

Unlike normal functions, where we cannot peek inside their body, Gobra learns the body of pure functions when calling them. The following assertions pass, without having specified a postcondition.

func client1(n int) {
    if n > 1 {
        // @ assert fibonacci(n) == fibonacci(n-1) + fibonacci(n-2)
    } else if n == 0 {
        // @ assert fibonacci(n) == 0
    }
}

Note that this does not automatically happen for the recursive calls in the body. For example, we can assert fibonacci(3) == fibonacci(2) + fibonacci(1), but not fibonacci(3) == 2.

func client2() {
    // @ assert fibonacci(3) == fibonacci(2) + fibonacci(1)
    // @ assert fibonacci(3) == 2
}

ERROR Assert might fail. 
Assertion fibonacci(3) == 2 might not hold.

By providing additional proof goals, we can to assert fibonacci(3) == 2. Having previously asserted fibonacci(1) == 1 and fibonacci(2) == 1, these can be substituted in fibonacci(3) == fibonacci(2) + fibonacci(1).

func client3() {
    // @ assert fibonacci(0) == 0
    // @ assert fibonacci(1) == 1
    // @ assert fibonacci(2) == 1
    // @ assert fibonacci(3) == 2
}

Exercise: iterative Fibonacci

We leave it as an exercise to provide invariants for an iterative implementation satisfying the specification.

Ghost and pure functions

Often, we will mark a function both ghost and pure. Although the concept of pure and ghost functions is orthogonal: a function may be ghost, pure, ghost and pure, or neither. Note that a ghost function may have side effects, e.g. modifying a ghost variable.

Termination of pure functions

By now we know that pure functions can be used in specifications, and since they do not have side effects nor non-determinism, they can be thought of as mathematical functions. To prevent inconsistencies, termination measures must be provided for pure functions:

pure
ensures res != 0
func incons(x int) (res int) {
    return 2 * incons(x)
}

All pure or ghost functions and methods must have termination measures, but none was found for this member.
pure

Next, we show why it is a bad idea to have non-terminating specification functions and derive assert false. For this we assume that incons terminates by giving it the wildcard termination measure decreases _.

pure
decreases _ // assuming termination
ensures res != 0
func incons(x int) (res int) {
    return 2 * incons(x)
}

func foo() {
    assert incons(1) == 2 * incons(1) // (1)
    assert incons(1) / incons(1) == 2 // (2)
    assert 1 == 2                     // (3)
    assert false
}

The assertions all pass since

1. We saw that we can replace the call of a pure function with its body.
2. Divide both sides by incons(1) (without the precondition ensures res != 0, Gobra reports the error Divisor incons(1) might be zero.)
3. Arithmetic
4. We found the contradiction 1 == 2, or equivalently false.

Permission to write

Permissions allow us to reason about aliased data in a modular way. Reading from and writing to a location is permitted based on the permission amount held. Write access is exclusive, i.e. permission to write to a location can only be held once. Permissions can be transferred between functions/methods, loop iterations, and they are gained on allocation.

Consider the following program. Should the assertion snapshotX == *x pass?

func inc(p *int) {
	*p = *p + 1
}

func client(x, y *int) {
	snapshotX := *x
	snapshotY := *y
	inc(y)
	// @ assert snapshotX == *x
}

If x and y were aliases, *x might be modified. Even if they are not aliases, we could not exclude the possibility that *x could somehow get modified since the body of inc is unknown when modularly verifying client.

Therefore it is important that the contract of a function specifies what might be modified by this function. In particular, this tells us what does not change without us having to explicitly specify it. Given x != y and that inc(y) might only modify *y, the assertion snapshotX == *x shall hold before and after the call inc(y).

So far, the program is rejected by Gobra:

ERROR Assignment might fail. 
Permission to *x might not suffice.

ERROR Assignment might fail. 
Permission to *p might not suffice.

In order to read and write the value stored at the memory address x, we must hold full access to this location. This is denoted by the accessibility predicate acc(x).

// @ requires acc(p)
func inc(p *int) {
	*p = *p + 1
}

// @ requires acc(x) && acc(y)
func client(x, y *int) {
	snapshotX := *x
	snapshotY := *y
	inc(y)
	// @ assert snapshotX == *x
}

Permissions are a solution to the problem described above. Now inc requires acc(p), which gives us an upper bound on what could be modified after the call. In the function client, the permissions acc(x) and acc(y) are held from the precondition. acc(y) is transferred when calling inc(y). Because acc(x) is kept, and write permission is exclusive, we can frame the condition snapshotX == *x holds across the call inc(y).

Moreover, permissions are used by Gobra to ensure that programs do not have data races, i.e., concurrent accesses to the same memory location with at least one modifying access. As a short teaser for concurrency:

func inc(p *int) {
	*p = *p + 1
}

// @ requires acc(p)
func driver(p *int) {
	go inc(p)
	go inc(p) // error
}

ERROR Precondition of call might not hold. 

go inc(p) might not satisfy the precondition of the callee.

Permission for pointers

Permissions are held for resources. For now, we only consider pointers. Having access acc(x) to a pointer x implies x != nil, so reading (e.g. tmp := *x) and writing (e.g. *x = 1) do not panic. Let us illustrate this with a function that swaps the values of two integer pointers:

func swap(x *int, y *int) {
	tmp := *x
	*x = *y
	*y = tmp
}

Go provides memory safety and prevents access to invalid memory. Similar to out-of-bounds array indices, a runtime error occurs when we call swap(nil, x):

panic: runtime error: invalid memory address or nil pointer dereference
[signal SIGSEGV: segmentation violation code=0x1 addr=0x0 pc=0x466c23]

goroutine 1 [running]:
main.swap(...)
        /gobra/swap.go:8
main.main()
        /gobra/swap.go:14 +0x3
exit status 2

Gobra detects this statically. Without holding access yet, we get the error:

Assignment might fail. 
Permission to *x might not suffice.

The permissions a function requires must be specified in the precondition. Since swap modifies both x and y, we write:

// @ requires acc(x) && acc(y)
func swap(x *int, y *int) {
	tmp := *x
	*x = *y
	*y = tmp
}

func client() {
	x := new(int)
	y := new(int)
	// @ assert acc(x)
	// @ assert acc(y)
	*x = 1
	*y = 2
	swap(x, y)
	// @ assert *x == 2 // fail
	// @ assert *y == 1
}

ERROR Assert might fail. 
Permission to *x might not suffice.

In our example, permissions acc(x) and acc(y) are obtained in client when they are allocated with new, then transferred when calling swap(x, y). With assert acc(x), we can check whether the permission is held. We add the postcondition acc(x) && acc(y) to transfer the permissions back to the caller when the function returns. Otherwise the permissions are leaked (lost).

old state

To specify the behavior of swap, we have to refer to the values *x and *y before any modifications. With old(*y), we can use the value of *y from the state at the beginning of the function call.

// @ requires acc(x) && acc(y)
// @ ensures acc(x) && acc(y)
// @ ensures *x == old(*y) && *y == old(*x)
func swap(x *int, y *int) {
	tmp := *x
	*x = *y
	*y = tmp
}

Exclusivity and aliasing

Clients may want to call swap with the same argument, e.g. swap(x, x). So far, our specification forbids this and we get the error:

// @ requires acc(x) && acc(y)
// @ ensures acc(x) && acc(y)
// @ ensures *x == old(*y) && *y == old(*x)
func swap(x *int, y *int) {
	tmp := *x
	*x = *y
	*y = tmp
}

func client2() {
	x := new(int)
	y := new(int)
	*x = 1
	*y = 2
	swap(x, x)
	// @ assert *x == 1
}

Precondition of call swap(x, x) might not hold. 
Permission to y might not suffice.

Having acc(x) && acc(y) implies x != y since we are not allowed to have write access to the same location. As a result, the precondition prevents us from calling swap(x, x).

One possibility is to perform a case distinction in the specification on x == y. While this works, the resulting specs are verbose, and we better refactor them to a reduced form.

// @ requires x == y ==> acc(x)
// @ requires x != y ==> acc(x) && acc(y)
// @ ensures x == y ==> acc(x)
// @ ensures x != y ==> acc(x) && acc(y)
// @ ensures x != y ==> *x == old(*y) && *y == old(*x)
// @ ensures x == y ==> *x == old(*x)
func swap(x *int, y *int) {
	tmp := *x
	*x = *y
	*y = tmp
}

1. acc(x) is needed in any case, hence it can be factored out

   // @ requires x == y ==> acc(x)
   // @ requires x != y ==> acc(x) && acc(y)
   // @ ensures x == y ==> acc(x)
   // @ ensures x != y ==> acc(x) && acc(y)
   

   becomes

   // @ requires acc(x)
   // @ requires x != y ==> acc(y)
   // @ ensures acc(x)
   // @ ensures x != y ==> acc(y)
   

2. Simplify the postconditions

   // @ ensures x != y ==> *x == old(*y) && *y == old(*x)
   // @ ensures x == y ==> *x == old(*x)
   

   with:

   // @ ensures *x == old(*y) && *y == old(*x)
   

   where the assertion is unchanged for the case x != y and we see it is equivalent for the case x == y by substituting y with x.

In the following subsection we additionally reduce the specification. At the end of this section you can find the final contract which allows calling swap even in cases where x and y are aliases.

Preserving memory access (preserves)

It is a common pattern that a function requires and ensures the same permissions. In our example, acc(x) and x != y ==> acc(y) is both required and ensured:

// @ requires acc(x)
// @ requires x != y ==> acc(y)
// @ ensures acc(x)
// @ ensures x != y ==> acc(y)

We can simplify this using the keyword preserves, which is syntactical sugar for requiring and ensuring the same assertion.

// @ preserves acc(x)
// @ preserves x != y ==> acc(y)

Final version of swap

// @ preserves acc(x)
// @ preserves x != y ==> acc(y)
// @ ensures *x == old(*y) && *y == old(*x)
func swap(x *int, y *int) {
	tmp := *x
	*x = *y
	*y = tmp
}

func client2() {
	x := new(int)
	y := new(int)
	*x = 1
	*y = 2
	swap(x, x)
	// @ assert *x == 1
	swap(x, y)
	// @ assert *x == 2
	// @ assert *y == 1
}

Self-framing assertions

Assertions in Gobra must be well-defined. This includes the fact that array indices in specifications must be in bounds. Operations like division have conditions under which they are well-defined. For a / b to be well-defined, b != 0 must hold. In the context of permissions, we get a new requirement that assertions are self-framing, i.e. access to all locations being read is required. Gobra checks that assertions are self-framing, and reports an error otherwise.

This also applies to contracts. In the following example, there is an error since *x and *y are accessed in the postcondition of swap, without holding permissions for x and y:

// @ requires acc(x) && acc(y)
// @ ensures *x == old(*y) && *y == old(*x)
func swap(x *int, y *int) {
	tmp := *x
	*x = *y
	*y = tmp
}

ERROR Method contract is not well-formed. 
Permission to *x might not suffice.

We can make it self-framing by returning the permissions acc(x) and acc(y):

// @ requires acc(x) && acc(y)
// @ ensures acc(x) && acc(y)   // <------ added
// @ ensures *x == old(*y) && *y == old(*x)
func swap(x *int, y *int) {
	tmp := *x
	*x = *y
	*y = tmp
}

Note that the order of the pre- and postconditions matters. The contract is checked from top to bottom and permission must be held before accessing. For example, if we exchange the postconditions of swap, we get the same error again:

// @ requires acc(x) && acc(y)
// @ ensures *x == old(*y) && *y == old(*x)
// @ ensures acc(x) && acc(y)
func swap(x *int, y *int) {
	tmp := *x
	*x = *y
	*y = tmp
}

ERROR Method contract is not well-formed. 
Permission to *x might not suffice.

Conjunctions are evaluated from left to right. As a result,

ensures acc(x) && acc(y) && *x == old(*y)

is self-framing, while the following is not:

ensures *x == old(*y) && acc(x) && acc(y)

As an exception, the assertion from an assert statement must not be self-framing. For example, we can write *x == 1 instead of acc(x) && *x == 1. However, Gobra reports an error if acc(x) is not held in the state.

func client() {
	x := new(int)
	*x = 1
	// @ assert *x == 1
	// @ assert acc(x) && *x == 1
}

Well-defined assertions that require access to all locations being read are called self-framing. Gobra checks that assertions are self-framing, and reports an error otherwise.

Addressability, @ and sharing

If we try to take the address of a local variable, Gobra reports an error:

func main() {
	b := 1
	x := &b
}

property error: got b that is not effective addressable
	x := &b
		^

To reference local variables, they must be marked as shared by appending the ampersand symbol to a variable name. Then Gobra uses permissions to track access to this location. For a variable b, we either write b /*@@@*/ using an inline annotation, or equivalently as b@ in .gobra files.

func main() {
	b /*@@@*/ := 1
	// b@ := 1 // .gobra version
	x := &b
	inc(x)
	// @ assert b == 2
}

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

With a pointer, a variable can be modified outside the function where it is defined. Note that otherwise, permissions are not required to reason about local variables. When passed as arguments to functions, the values are copied, and the original variables are not modified.

Sharing applies to local variables of any type. In this section, we specifically look at shared structs. An example with shared arrays is shown in a following section.

Shared structs

The fields of structs can 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.

type Coord struct {
	x, y int
}

// @ requires acc(&c.x) && acc(&c.y)
// @ ensures acc(&c.x) && acc(&c.y)
// @ 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
}


func client1() {
	c := Coord{1, 2}
	c.Scale(5)
	// @ assert c == Coord{5, 10}
}

ERROR Scale requires a shared receiver ('share' or '@' annotations might be missing).

Gobra reports an error if we try to call Scale on a non-shared struct. Scale is defined for a pointer receiver, and here the address of the struct is taken implicitly. The error message is instructive, and we can fix this by marking c as shared:

func client1() {
	c /*@@@*/ := Coord{1, 2} // changed
	c.Scale(5)
	// @ assert c == Coord{5, 10}
}

Composite literals are addressable. We may reference them directly without errors:

func client2() {
	c := &Coord{1, 2}
	c.Scale(5)
	// @ assert *c == Coord{5, 10}
}

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.

func client3(c1, c2 Coord) {
	c1.Scale(5) // error
	c2.Scale(-1) // error
}

ERROR Scale requires a shared receiver ('share' or '@' annotations might be missing).
	c1.Scale(5)
    ^
ERROR Scale requires a shared receiver ('share' or '@' annotations might be missing).
	c2.Scale(-1)
    ^

Parameters of a function or method can be shared with the share statement at the beginning of the body.

func client3(c1, c2 Coord) {
	// @ share c1, c2  // <--- added
	c1.Scale(5)
	c2.Scale(-1)
}

This resolves the errors above.

Permission to read

So far we have seen permissions of the form acc(x) for a pointer x. We can be more specific and give a permission amount as the second argument to acc, as a fractional number. In this case, we speak of fractional permissions:

• A permission amount of 1 allows us to read and write (e.g. acc(x, 1), or equivalently acc(x), acc(x, writePerm), acc(x, 1/1))
• A positive amount < 1 allows only reading (e.g. acc(x, 1/2), acc(x, 3/4))
• No access is denoted as acc(x, 0) or equivalently acc(x, noPerm).
• A permission amount > 1 for a pointer is a contradiction and implies false.

If a function requires write permission, and yet we want to guarantee that the value stored at the locations remains unchanged, an extra postcondition must be added. Requiring only read permission, a caller retaining a positive permission amount can guarantee across the call that the value remained unchanged.

Permission amounts to the same location can be split up, for example acc(x, 3/4) is equivalent to acc(x, 1/4) && acc(x, 1/4) && acc(x, 1/4). Moreover, this is useful for concurrency since it allows us to split read permissions to multiple threads and guarantee that there can only be one thread alive with exclusive write permission to a location ¹.

In the remainder of this section, we study how to use fractional permissions with examples.

Previously we saw the function swap that needs write access to both variables. In the following example, we sum the fields left and right of a struct pair. Since we only read the fields, we specify a permission amount of 1/2.

type pair struct {
	left, right int
}

// @ preserves acc(&p.left, 1/2) && acc(&p.right, 1/2)
// @ ensures s == p.left + p.right
func (p *pair) sum() (s int) {
	return p.left + p.right
}

func client() {
	p := &pair{3, 5}
	res := p.sum()
	// @ assert p.left == 3 && p.right == 5
	// @ assert res == 8
}

Note that we specify access to the struct fields as acc(&p.left) and not acc(p.left) as p.left is a value of type integer, but access is held to a resource (in this case, a pointer). For a pointer p to a struct, we can additionally use the syntactic sugar acc(p, 1/2), which denotes permission of 1/2 to all fields of the struct. Concretely we can replace in our example

// @ preserves acc(&p.left, 1/2) && acc(&p.right, 1/2)`

with

// @ preserves acc(p, 1/2)

Framing properties

Since sum requires only acc(p, 1/2), and client acquires full access on allocation, we can frame the property p.left == 3 && p.right == 5 across the call p.sum(), without specifying that the shared struct is not modified.

// @ preserves acc(p, 1/2)
// @ ensures s == p.left + p.right
func (p *pair) sum() (s int) {
	return p.left + p.right
}

func client() {
	p := &pair{3, 5}
	res := p.sum()
	// @ assert p.left == 3 && p.right == 5
	// @ assert res == 8
}

But if we change client to get only permission amount 1/2 for p, Gobra reports an error.

// @ requires acc(p, 1/2)
// @ requires p.left == 0
func client2(p *pair) {
	res := p.sum()
	// @ assert p.left == 0
}

Assert might fail. 
Assertion p.left == 0 might not hold.

The method sum requires acc(p, 1/2), which must be transferred by the caller. To frame the property p.left == 0 across the call, the caller must retain a non-negative permission amount to prevent write access. One way is to require a higher permission amount like 3/4. Then client keeps acc(p, 1/4) across the call and we are sure that p.left is not modified.

// @ requires acc(p, 3/4)
// @ requires p.left == 0
func client3(p *pair) {
	res := p.sum()
	// @ assert p.left == 0
}

Now let us consider sum with a different contract, where write access is required:

type pair struct {
	left, right int
}

// @ preserves acc(&p.left, 1) && acc(&p.right, 1)
// @ ensures s == p.left + p.right
// @ ensures p.left == old(p.left) && p.right == old(p.right)
func (p *pair) sum() (s int) {
	return p.left + p.right
}

func client() {
	p := &pair{3, 5}
	res := p.sum()
	// @ assert p.left == 3 && p.right == 5
	// @ assert res == 8
}

For the assertions in client to pass, we specify that sum does not modify the fields of the pair with the postcondition p.left == old(p.left) && p.right == old(p.right).

Fractional permissions and pointers

For a pointer x, for any positive permission amount p, acc(x, p) implies x != nil. But acc(x1, 1/2) && acc(x2, 1/2) does no longer imply x1 != x2. If we have 2/3 fractional permission to x1 instead, we can now infer x1 != x2 since permission amounts to the same location are added together:

requires acc(x1, 2/3) && acc(x2, 1/2)
ensures x1 != x2
func lemma(x1, x2 *int) {}

Access predicates are not duplicable

In classical logic, if the proposition \( P \) holds then clearly the proposition \( P \land P\) holds as well. For assertions containing access predicates, this does no longer hold. Consider acc(p, 1/2), which denotes read permission, and acc(p, 1/2) && acc(p, 1/2), which implies write permission acc(p, 1).

// @ requires acc(p, 1/2)
func reader(p *int) {
	// ...
}

// @ requires acc(p, 1)
func driver(p *int) {
	go reader(p)
	go reader(p)
}

Wildcard permission

The permission amount _ stands for an arbitrary positive permission amount. Since the specific amount is unspecified, holding acc(p, _) enables reading but not writing.

By requiring acc(p, _), we can make the method sum more versatile, allowing it to be called in cases where we have, for example only acc(p, 1/4) instead of acc(p, 1/2):

type pair struct {
	left, right int
}

// @ requires acc(p, _)
// @ ensures acc(p, _)
// @ ensures s == p.left + p.right
// @ ensures p.left == old(p.left) && p.right == old(p.right)
func (p *pair) sum() (s int) {
	return p.left + p.right
}

// @ requires acc(p1, 1/2)
// @ requires acc(p2, 1/4)
func client1(p1, p2 *pair) {
	p1.sum()
	p2.sum()
}

However, this comes with the drawback that we cannot recover the exact permission amounts. As seen in the following client code, where we lose write access, meaning p.left and p.right can no longer be modified. The postcondition acc(p, _) ensures only that an unspecified positive permission amount is transferred back to the caller, but does not guarantee that it matches the unspecified positive permission amount that the caller initially transferred.

func client() {
	p := &pair{3, 5}
	res := p.sum()
	// @ assert p.left == 3 && p.right == 5
	p.left = p.right // Error
	p.right = res
	// @ assert p.left == 5 && p.right == 8
}

ERROR Assignment might fail. 
Permission to p.left might not suffice.

Please also note that, in order to frame the property

// @ assert p.left == 3 && p.right == 5

we have to include the following postcondition. From the perspective of the caller, an unspecified permission amount could also include write permission.

// @ ensures p.left == old(p.left) && p.right == old(p.right)

Permission type and parameter

Having a fixed permission amount in the contract is restrictive. For example, clients with only acc(r, 1/4) cannot call p.sum():

type pair struct {
	left, right int
}

// @ requires acc(p, 1/2)
// @ ensures acc(p, 1/2)
// @ ensures s == p.left + p.right
func (p *pair) sum() (s int) {
	return p.left + p.right
}

// @ requires acc(p, 1/4)
// @ requires p.left == 2 && p.right == 3
func client(p *pair) {
	res := p.sum()
	// @ assert res == 5
}

ERROR Precondition of call p.sum() might not hold. 
Permission to p might not suffice.

One option is to use the wildcard permission amount, as previously studied, which comes with its own drawbacks. In this section, we show how to abstract the exact permission amount by introducing a ghost parameter of type perm, i.e. Gobra's type for permission amounts:

type pair struct {
	left, right int
}

// @ requires a > 0	    // <--- added
// @ requires acc(p, a) // <--- changed
// @ ensures acc(p, a)	// <--- changed
// @ ensures s == p.left + p.right
func (p *pair) sum( /*@ ghost a perm @*/ ) (s int) { // <--- new parameter
	return p.left + p.right
}

// @ requires acc(p, 1/2)
// @ requires p.left == 2 && p.right == 3
func client(p *pair) {
	res := p.sum( /*@ 1/4 @*/ )  // <--- changed
	// @ assert res == 5
}

Conventionally the permission amount is called p, which clashes here with our pair pointer. When calling sum, we must pass the permission amount: p.sum( /*@ 1/4 @*/ ). The precondition p > 0 is important to get read permission, otherwise we get:

ERROR Method contract is not well-formed.
Expression p might be negative.

Permission arithmetic

We may convert a fraction to a permission amount and perform calculations with it:

func main() {
	assert perm(1/2) + perm(1/2) == writePerm
	assert perm(1) - 1/2 == perm(1/2)
	assert perm(1/2) * 0 == noPerm
	assert perm(1) / 2 != writePerm
	assert perm(1/3) == 1/3
	assert perm(perm(1/3)) == perm(1/3)
}

Note that for access predicates, we can, and have been using the shorthand acc(p, 1/2) instead of acc(p, perm(1/2)).

Inhaling and exhaling

Permissions can be added to the verification state by inhaling, and removed by exhaling. This can be useful for debugging but should not be needed for normal verification purposes.

Removing permissions with exhale

The statement exhale ASSERTION

1. checks that all value constraints in ASSERTION hold, otherwise an error is reported.
2. checks that all permissions mentioned by ASSERTION are held, otherwise an error is reported.
3. removes all permissions mentioned by ASSERTION

Exhale is similar to assert, with the difference that assert does not remove any permissions:

requires acc(x, 1)
func breatheOut(x *int) {
	assert acc(x, 1)
	exhale acc(x, 1/4)
	assert acc(x, 3/4)
	assert acc(x, 3/4) // no permission removed
	exhale acc(x, 1) // error
}

ERROR Exhale might fail. 
Permission to x might not suffice.

The last exhale failed since at this point only a permission amount of 3/4 is held.

Adding permissions with inhale

The statement inhale ASSERTION

1. adds all permissions mentioned by ASSERTION
2. assumes all value constraints in ASSERTION hold

requires acc(x, 1/2)
func breatheIn(x *int) {
	assert acc(x, 1/2)
	inhale acc(x, 1/2)
	assert acc(x, 1/1)
}

By inhaling a permission amount of 1 for the pointer x while already holding acc(x, 1/2), we reach an inconsistent state, and false can be asserted:

requires acc(x, 1/2)
func breatheMore(x *int) {
	inhale acc(x, 1)
	assert acc(x, 3/2)
	assert false
}

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)

Pure functions and permissions

Recall that pure functions have no side effects. Hence, they must not leak any permissions and implicitly return all permissions mentioned in the precondition. While pure functions can require write permission, they cannot actually modify values, as this would be a side effect.

The pure and ghost function allZero returns whether all elements of an array behind a pointer are zero. After allocation with new, the array is filled with zero values, and this can be asserted.

package ghostpure

const N = 42
/*@
ghost
requires forall i int :: 0 <= i && i < len(*s) ==> acc(&((*s)[i]))
decreases
pure func allZero(s *[N]int) bool {
    return forall i int :: 0 <= i && i < len(*s) ==> (*s)[i] == 0
}
@*/

func client() {
    xs := new([N]int)
    // @ assert allZero(xs)
    // implicitly transferred back
    // @ assert acc(xs)
}

Pure functions implicitly return all permissions mentioned in the precondition.

Slices

Slices provide an abstraction over a contiguous sequence of data. A slice has a length, a capacity, and uses an underlying array as storage.

In the following example, a constant n is added to all elements of a slice. Note that the functions len and cap may be used in contracts. Access to slice elements is specified using quantified permissions. We obtain permission to the slice elements on allocation, here with make. Note that the loop must preserve the permissions with an invariant.

// @ preserves forall k int :: {&s[k]} 0 <= k && k < len(s) ==> acc(&s[k])
// @ ensures forall k int :: {&s[k]} 0 <= k && k < len(s) ==> s[k] == old(s[k]) + n
func addToSlice(s []int, n int) {
	// @ invariant 0 <= i && i <= len(s)
	// @ invariant forall k int :: {&s[k]} 0 <= k && k < len(s) ==> acc(&s[k])
	// @ invariant forall k int :: {&s[k]} i <= k && k < len(s) ==> s[k] == old(s[k])
	// @ invariant forall k int :: {&s[k]} 0 <= k && k < i ==> s[k] == old(s[k]) + n
	for i := 0; i < len(s); i += 1 {
		s[i] = s[i] + n
	}
}

func client() {
	s := make([]int, 4, 8)
	// @ assert len(s) == 4 && cap(s) == 8
	addToSlice(s, 1)
	// @ assert forall i int :: {&s[i]} 0 <= i && i < 4 ==> s[i] == 1
}

After initialization with a literal, we also gain permission.

s1 := []int{0, 1, 1, 2, 3, 5}
// @ assert forall i int :: {&s1[i]} 0 <= i && i < len(s1) ==> acc(&s1[i])

Syntactic sugar for slice access

For a slice s1, acc(s1) is syntactic sugar for:

forall i int :: {&s1[i]} 0 <= i && i < len(s1) ==> acc(&s1[i])

The assert statements are equivalent:

s1 := []int{0, 1, 1, 2, 3, 5}
// @ assert forall i int :: {&s1[i]} 0 <= i && i < len(s1) ==> acc(&s1[i])
// @ assert acc(s1)

Slicing

A slice can be created from another slice or array by slicing it, in general with an expression of the form a[i:j:k]. To check slicing does not panic, Gobra checks as part of the contract of the slicing operation that 0 <= i && i <= j && j <= k && k <= cap(a) holds.

We may create two overlapping slices l and r but run into a permission error:

func overlappingFail() {
	s := make([]int, 3)
	l := s[:2]
	r := s[1:]
	addToSlice(l, 1)
	addToSlice(r, 1) // error
}

ERROR Assert might fail. 
Permission to r might not suffice.

While we cannot assert acc(l) && acc(r), to call addToSlice we only need permission for either of the slices, and it should be possible to assert acc(l) and acc(r) separately. In order to get permission for the slice r, we must explicitly assert how the addresses to the elements of r relate to those of s:

assert forall i int :: {&r[i]} 0 <= i && i < len(r) ==> &r[i] == &s[i+1]

With this proof annotation, the function verifies:

func overlappingSucceed() {
	s := make([]int, 3)
	l := s[:2]
	r := s[1:]
	// @ assert forall i int :: {&r[i]} 0 <= i && i < len(r) ==> &r[i] == &s[i+1]
	addToSlice(l, 1)
	// @ assert s[0] == 1 && s[1] == 1
	addToSlice(r, 1)
	// @ assert r[0] == 2 && r[1] == 1
	// @ assert s[0] == 1 && s[1] == 2 && s[2] == 1
}

copy and append

Go includes the copy and append built-in functions.

We give the contracts for copy and append for a generic type T (Gobra does not yet support generics). In Gobra, we must pass an additional ghost parameter that specifies the permission amount required to read the elements of src. This allows the functions to generally be used independent of the exact permission amount

requires p > 0
requires forall i int :: {&src[i]} 0 <= i && i < len(src) ==> acc(&src[i])
requires forall i int :: {&xs[i]} 0 <= i && i < len(xs) ==> acc(&xs[i], p)
ensures len(res) == len(src) + len(xs)
ensures forall i int :: {&res[i]} 0 <= i && i < len(res) ==> acc(&res[i])
ensures forall i int :: {&xs[i]} 0 <= i && i < len(xs) ==> acc(&xs[i], p)
ensures forall i int :: {&res[i]} 0 <= i && i < len(src) ==> res[i] === old(src[i])
ensures forall i int :: {&res[i]} len(src) <= i && i < len(res) ==> res[i] === xs[i - len(src)]
func append[T any](ghost p perm, src []T, xs ...T) (res []T)

Note that since append is variadic, the permission amount must be the first argument. The permission to src is lost, as the underlying array could be reallocated if the capacity is not sufficient to append the new elements. s = append(s, 42) is a common pattern in Go, and this way permissions to s are preserved.

copy copies the elements from src to dst. It stops when the end of the shorter slice is reached and returns the number of elements copied.

requires 0 < p
requires forall i int :: {&dst[i]} (0 <= i && i < len(dst)) ==> acc(&dst[i], write)
requires forall i int :: {&src[i]} (0 <= i && i < len(src)) ==> acc(&src[i], p)
ensures len(dst) <= len(src) ==> res == len(dst)
ensures len(src) < len(dst) ==> res == len(src)
ensures forall i int :: {&dst[i]} 0 <= i && i < len(dst) ==> acc(&dst[i], write)
ensures forall i int :: {&src[i]} 0 <= i && i < len(src) ==> acc(&src[i], p)
ensures forall i int :: {&dst[i]} (0 <= i && i < len(src) && i < len(dst)) ==> dst[i] === old(src[i])
ensures forall i int :: {&dst[i]} (len(src) <= i && i < len(dst)) ==> dst[i] === old(dst[i])
func copy[T any](dst, src []T, ghost p perm) (res int)

The permissions amount must be explicitly passed as perm(1/2) instead of only 1/2. This simple example shows the usage of copy and append:

s1 := []int{1, 2}
s2 := []int{3, 4, 5}

s0 := make([]int, len(s1))
copy(s0, s1 /*@, perm(1/2) @*/)
// @ assert forall i int :: {&s0[i]} {&s1[i]} 0 <= i && i < len(s0) ==> s0[i] == s1[i]

s3 := append(/*@ perm(1/2), @*/ s1, s2...)
s4 := append(/*@ perm(1/2), @*/ s0, 3, 4, 5)
// @ assert forall i int :: {&s3[i]} {&s4[i]} 0 <= i && i < len(s3) ==> s3[i] == s4[i]

Using the nil slice, we could refactor the make and copy operations into the single line s0 := append([]int(nil), s1...). As opposed to the nil pointer, we may hold permission for the nil slice:

var s2 []int
// @ assert acc(s2)
// @ assert s2 == nil && len(s2) == 0 && cap(s2) == 0

In Go it is possible to append a slice to itself. The contract of append forbids this.

s1 := []int{1, 2}
s2 := append(/*@ perm(1/64), @*/ s1, s1...)

ERROR Precondition of call append(  perm(1/64),  s1, s1...) might not hold. 
Permission to append(  perm(1/64),  s1, s2...) might not suffice

Similarly, in Go the behavior of copy is independent of whether the underlying memory of the slices overlaps. Again, Gobra's contract of copy forbids this:

s := []int{1, 2, 3, 4}
s1 := s[1:]
// @ assert acc(s1)
copy(s, s1 /*@, perm(1/2) @*/)
// fmt.Println(s) // [2 3 4 4]

ERROR Precondition of call copy(s, s1 , perm(1/2) ) might not hold. 
Permission to copy(s0, s1 , perm(1/2) ) might not suffice.

Range clause for slices

Gobra supports the range clause for slices. We refactor the loop in addToSlice:

// @ requires len(s) > 0
// @ preserves acc(s)
// @ ensures forall k int :: {&s[k]} 0 <= k && k < len(s) ==> s[k] == old(s[k]) + n
func addToSlice(s []int, n int) {
	// @ invariant acc(s)
	// @ invariant forall k int :: {&s[k]} i0 <= k && k < len(s) ==> s[k] == old(s[k])
	// @ invariant forall k int :: {&s[k]} 0 <= k && k < i0 ==> s[k] == old(s[k]) + n
	for i, e := range s /*@ with i0 @*/ {
		s[i] = e + n
	}
}

Note that we added the precondition len(s) > 0. Otherwise there is the error:

ERROR Loop invariant might not be established. 
Permission to s[k] might not suffice.

For the case where len(s) == 0, i, e and i0 are never assigned values. As a result, the second invariant cannot be established because i0 is arbitrary. For example, s[k] could be instantiated as s[-1], even though no permission is held for &s[-1].

Alternatively, we could handle the empty case specifically:

// @ preserves acc(s)
// @ ensures forall k int :: {&s[k]} 0 <= k && k < len(s) ==> s[k] == old(s[k]) + n
func addToSlice(s []int, n int) {
	if len(s) == 0 {
		return
	}
	// ...
	// @ invariant acc(s)
	// @ invariant forall k int :: {&s[k]} i0 <= k && k < len(s) ==> s[k] == old(s[k])
	// @ invariant forall k int :: {&s[k]} 0 <= k && k < i0 ==> s[k] == old(s[k]) + n
	for i, e := range s /*@ with i0 @*/ {
		s[i] = e + n
	}
}

Binary search over slices

We conclude this section by revisiting the binary search example. Now we can perform a BinarySearch sorted slices of arbitrary length for a target value. This version is more efficient because no arrays need to be copied.

We define a pure and ghost function isSliceSorted, to use in the contract of BinarySearch. Unlike BinarySearchArr, we add a condition to handle the empty slice and specify access to the slice elements.

package binarysearchslice

/*@
ghost
requires forall i int :: {&s[i]} 0 <= i && i < len(s) ==> acc(&s[i], 1/2)
decreases
pure func isSliceSorted(s []int) bool {
	return forall i, j int :: {&s[i], &s[j]} 0 <= i && i < j && j < len(s) ==> s[i] <= s[j]
}
@*/

// @ requires forall i int :: {&s[i]} 0 <= i && i < len(s) ==> acc(&s[i], 1/2)
// @ requires isSliceSorted(s)
// @ ensures forall i int :: {&s[i]} 0 <= i && i < len(s) ==> acc(&s[i], 1/2)
// @ ensures 0 <= idx && idx <= len(s)
// @ ensures idx > 0 ==> s[idx-1] < target
// @ ensures idx < len(s) ==> target <= s[idx]
// @ ensures found == (idx < len(s) && s[idx] == target)
func BinarySearch(s []int, target int) (idx int, found bool) {
	if len(s) == 0 {
		return 0, false
	}
	low := 0
	high := len(s)
	mid := 0
	// @ invariant forall i int :: {&s[i]} 0 <= i && i < len(s) ==> acc(&s[i], 1/2)
	// @ invariant 0 <= low && low <= high && high <= len(s)
	// @ invariant 0 <= mid && mid < len(s)
	// @ invariant low > 0 ==> s[low-1] < target
	// @ invariant high < len(s) ==> target <= s[high]
	for low < high {
		// fmt.Println(low, high, s[:low], s[low:high], s[high:])
		mid = (low + high) / 2
		if s[mid] < target {
			low = mid + 1
		} else {
			high = mid
		}
	}
	// fmt.Println(low, high, s[:low], s[low:high], s[high:])
	return low, low < len(s) && s[low] == target
}

func client() {
	s := []int{0, 1, 1, 2, 3, 5, 8}
	i1, found1 := BinarySearch(s, 1)
	// @ assert found1 && s[i1] == 1 && i1 == 1
	i2, found2 := BinarySearch(s, 2)
	// @ assert found2 && s[i2] == 2 && i2 == 3
	i4, found4 := BinarySearch(s, 4)
	// @ assert !found4 && i4 == 5
	i10, found10 := BinarySearch(s, 10)
	// @ assert !found10 && i10 == len(s)
}

Maps

Go provides the built-in map data structure implementing a hash table.

watched := make(map[string]bool, 10) // optional capacity
// @ assert acc(watched) && len(watched) == 0

Permission to a map is obtained on allocation, e.g. from make. The accessibility predicate acc(watched) is for the entire map. Individual elements, as in slices, are not addressable.

Holding write permissions, we can add entries. In specifications, we can check with in if a key is contained in the map.

watched["Blade Runner"] = true
// @ assert "Blade Runner" in watched && len(watched) == 1

The values can be retrieved with their keys. Note that key elements must be comparable. For example, one cannot use other maps, slices, and functions as keys.

elem, ok := watched["Blade Runner"]
// @ assert ok && elem
// non-existing key
elem, ok := watched["Dune"]
// @ assert !ok && !elem

nil map

A nil map is obtained with new or by not initializing a map variable. No permission is held for the nil map and no elements can be added. Otherwise, it behaves like an empty map.

var rating map[string]int
// @ assert acc(rating, noPerm)
// @ assert len(rating) == 0
r, ok := rating["Dune"]
// @ assert !ok && r == 0

rotten := new(map[string]int)
// @ assert len(*rotten) == 0

We can read from the nil map as we would from an empty map, even without permission. For functions that read from a map m, the precondition m != nil ==> acc(m, 1/2) is typically used to support both nil and non-nil maps.

Range clause for maps

Range loops iterate over the keys and values for a map. A with clause must be added (e.g. range m /*@ with visited @*/). The ghost variable visited is a mathematical set (introduced in the next chapter) that contains the keys already visited. In the following snippet, we build a map literal, with keys representing identifiers and Movie structs as values. The function avgRating computes the average rating of all movies in a map. We focus on the loop and omit the full functional specification for simplicity.

package movies

type Movie struct {
	name   string
	rating int
}

// @ requires acc(m, 1/2)
// @ requires len(m) > 0
func avgRating(m map[int]Movie) int {
	sum := 0
	// @ invariant acc(m, 1/2)
	// @ invariant len(m) > 0
	for _, movie := range m /*@ with visited @*/ {
		sum += movie.rating
	}
	return sum / len(m)
}

func critique() {
	nolan := map[int]Movie{
		132: {"Oppenheimer", 8},
		234: {"Tenet", 7},
		432: {"Dunkirk", 9},
	}
	// @ assert acc(nolan) && len(nolan) == 3
	avgRating(nolan) // 8
}

Go does not specify the iteration order over maps (see ¹). An entry added during iteration may either be produced or skipped. Gobra prohibits the mutation of maps while iterating.

package main

type Movie struct {
	name   string
	rating int
}

// @ requires acc(m)
func produceSequels(m map[int]Movie) {
	// @ invariant acc(m)
	for id, movie := range m /*@ with visited @*/ {
		m[2*id] = Movie{movie.name + "2", movie.rating - 2} // error
	}
}

func main() {
	movies := map[int]Movie{
		2: {"Jaws", 6},
		3: {"Cars", 5},
	}
	produceSequels(movies)
}

ERROR Assignment might fail. 
Permission to m might not suffice.

The output of the Go program is nondeterministic (two samples):

map[2:{Jaws 6} 3:{Cars 5} 4:{Jaws2 4} 6:{Cars2 3} 8:{Jaws22 2}]

map[2:{Jaws 6} 3:{Cars 5} 4:{Jaws2 4} 6:{Cars2 3} 12:{Cars22 1} 24:{Cars222 -1} 48:{Cars2222 -3} 96:{Cars22222 -5} 192:{Cars222222 -7} 384:{Cars2222222 -9}]

Mutation is prevented by exhaling a small constant permission amount to the map before the loop. As a consequence, the wildcard permission amount is insufficient:

// @ requires acc(m, _)
// @ requires len(m) > 0
func wildRating(m map[int]Movie) int {
	sum := 0
	// @ invariant acc(m, _)
	// @ invariant len(m) > 0
	for _, movie := range m /*@ with visited @*/ {
		sum += movie.rating
	}
	return sum / len(m)
}

ERROR Range expression should be immutable inside the loop body.
Permission to m might not suffice.

delete and clear

At the moment, Gobra does not support Go's built-in function delete for removing map entries or clear for removing all map entries.

Predicates

Predicates abstract over assertions, i.e., giving a name to a parametrized assertion. Predicates can be used for representing memory access to data structures of possibly unbounded size, such as linked lists or binary trees. While quantified permissions are often used to specify pointwise access, e.g. to elements of a slice, predicates are suitable to denote access to recursive data structures.

Running example: List

Throughout the sections of this chapter, we will follow the example of a List data structure for storing integer values, implemented as a singly linked list¹.

type List struct {
	// Pointer to the next element in the linked list.
	next *List
	// The value stored with this element.
	Value int
}

We will implement the following public API for the construction and manipulation of lists:

// Returns the empty list.
func Empty() (l *List)

// New creates a new List node with the specified value and tail.
func New(value int, tail *List) (out *List)

// Tail returns a new list that is the tail of the original list,
// excluding the first element.
func (l *List) Tail() (out *List)

// Remove returns the list with the element at index i deleted.
func (l *List) Remove(i int) (out *List)

// Head returns the value of the first element in the list.
func (l *List) Head() (value int)

// Get returns the element at index i in the list.
func (l *List) Get(i int) (value int)

// Returns true iff the list is empty.
func (l *List) IsEmpty() (empty bool) {

// Returns the length of the list.
func (l *List) Length() (length int)

In a first step, we focus only on specifying memory access. Then in the second step, the contracts are completed for functional correctness. The following client code will be verified in the final example:

func client() {
	ll := Empty()
	l0 := ll.Length()
	// @ assert l0 == 0
	ll = New(11, ll)
	// @ assert ll.Mem()
	// @ assert ll.Head() == 11
	// @ assert ll.View() == seq[int]{11}
	l1 := ll.Length()
	// @ assert l1 == 1
	ll = ll.Tail()
	// @ assert ll.View() == seq[int]{}
	ll = New(22, Empty())
	// @ assert ll.Head() == 22
	ll = New(33, ll)
	// @ assert ll.Head() == 33
	l2 := ll.Length()
	// @ assert l2 == 2
	v0 := ll.Get(0)
	v1 := ll.Get(1)
	// @ assert v0 == 33
	// @ assert v1 == 22
	ll := ll.Remove(1)
	l3 := ll.Length()
	// @ assert ll.Head() == 33
	// @ assert l3 == 1
}

Defining predicates

Here we define the predicate elements to represent access to all elements in a list l:

type List struct {
	// Pointer to the next element in the linked list.
	next *List
	// The value stored with this element.
	Value int
}


/*@
pred elements(l *List) {
	acc(&l.Value) && acc(&l.next) && (l.next != nil ==> elements(l.next))
}
@*/

Predicates are defined with the keyword pred and possibly with parameters. The body is a single self-framing assertion.

Note that elements is recursive, and represents access not only to acc(&l.Value) && acc(&l.next), but also to the elements in its tail.

A predicate instance is not equivalent to its body and we must explicitly exchange between the two with the fold and unfold statements, which we study next.

Constructing predicates with fold

The fold statement exchanges the body of a predicate for a predicate instance. In the following example we allocate a new list and highlight with asserts that the assertion from the body of elements holds for l. With the statement fold elements(l) we exchange these for the predicate instance elements(l) as a token representing access to the list. However, acc(&l.Value) has been exhaled and we may no longer access l.Value:

	l := &List{Value: 1, next: nil}
	// @ assert acc(&l.Value) && acc(&l.next) && l.next == nil
	// @ assert acc(&l.Value) && acc(&l.next) && (l.next != nil ==> elements(l.next))

	// @ fold elements(l)

	// @ assert elements(l)

	v := l.Value // error

ERROR Assignment might fail. 
Permission to l.Value might not suffice.

Folding fails if the assertion from the body does not hold:

// @ ensures elements(l)
func newFail(value int, tail *List) (l *List) {
	l := &List{Value: value, next: tail}
	// @ fold elements(l) // error
	return l
}

ERROR Fold might fail. 
Permission to elements(l.next) might not suffice.

We can fix this by requiring elements(tail) if tail != nil.

// @ requires tail != nil ==> elements(tail)
// @ ensures elements(l)
func newList(value int, tail *List) (l *List) {
	l := &List{Value: value, next: tail}
	// @ fold elements(l)
	return l
}

Unwrapping predicates with unfold

The unfold statement exchanges a predicate instance with its body.

	l := &List{Value: 1, next: nil}
	// @ fold elements(l)
	// @ assert elements(l)
	// @ unfold elements(l)
	// @ assert acc(&l.Value) && acc(&l.next) && (l.next != nil ==> elements(l.next))
	v := l.Value

Unfolding fails, if the predicate instance is not held. If we try to unfold elements(l) twice, the second statement causes an error:

	l := &List{Value: 1, next: nil}
	// @ fold elements(l)
	// @ unfold elements(l)
	// @ unfold elements(l) // error

ERROR Unfold might fail. 
Permission to elements(l) might not suffice.

Recursive predicates

Predicates can be recursive, as seen with elements. In the following example, we build a list with 3 elements, always folding the permissions. elements(l3) abstracts access to the full list and has the predicate instances elements(l2) and elements(l1) folded within it. We could continue this process, and handle a list of possibly unbounded size. To recover the concrete permissions, we unfold the predicates in the reverse order.

	l1 := &List{Value: 1, next: nil}
	// @ fold elements(l1)
	l2 := &List{Value: 2, next: l1}
	// @ fold elements(l2)
	l3 := &List{Value: 3, next: l2}
	// @ fold elements(l3)
	s := 0
	l := l3
	// @ assert elements(l)
	// @ invariant l != nil ==> elements(l)
	for l != nil {
		// @ unfold elements(l)
		s += l.Value
		l = l.next
	}

Please note that we lose access when traversing the list to sum the elements, which is undesirable.

Summary

Predicates abstract over assertions, i.e., giving a name to a parametrized assertion.

The fold statement exchanges the body of a predicate for a predicate instance. If the assertion in the body does not hold, an error is reported.

The unfold statement exchanges a predicate instance with its body. If the predicate instance is not held, an error is reported.

Abstracting memory access with predicates

In this section, we emphasize how predicates can abstract memory access, and help enforce the information hiding principle, hiding implementation details such as non-exported fields, memory layout, or other internal assumptions.

The core idea is that clients shall only need to hold predicate instances, allowing them to interact with an API without exposing specific permissions to fields. We exemplify this on a subset of the List API, for now focusing only on specifying memory access without proving functional correctness.

Previously, we defined the predicate elements:

/*@
pred elements(l *List) {
	acc(&l.Value) && acc(&l.next) && (l.next != nil ==> elements(l.next))
}
@*/

Predicates can be defined with a receiver, too. This conveniently couples the predicate to the type. As a convention, we choose the name Mem to signal that this predicate abstracts the memory.

type List struct {
	// Pointer to the next element in the linked list.
	next *List
	// The value stored with this element.
	Value int
}

/*@
// Represents access to the List element and all elements in its tail.
pred (l *List) Mem() {
	l != nil ==> (acc(l) && l.next.Mem())
}
@*/

Note the slight difference: for l.Mem(), l could be nil whereas elements(l) implies l != nil.

A predicate instance l.Mem() can be obtained, for example, by allocating a new list. The postconditions of Empty and New ensure this. For New, the contract in turn requires holding tail.Mem().

// Returns the empty list.
// @ ensures l.Mem()
// @ ensures l.IsEmpty()
func Empty() (l *List) {
	l = (*List)(nil)
	// @ fold l.Mem()
	return
}

// New creates a new List node with the specified value and tail.
// @ requires tail.Mem()
// @ ensures out.Mem()
// @ ensures !out.IsEmpty()
// @ ensures out.Head() == value
func New(value int, tail *List) (out *List) {
	out = &List{next: tail, Value: value}
	// @ fold out.Mem()
	return
}

Let us put this in contrast with the function NewBad:

// @ ensures acc(&out.Value) && acc(&out.next)
// @ ensures out.next == tail
// @ ensures out.Value == value
func NewBad(value int, tail *List) (out *List) {
	out = &List{next: tail, Value: value}
	return
}

The contract is bad in a number of ways:

• The field next is used in the contract although it is non-exported and clients of the package are not even aware of its existence.
• Internal decisions are leaked, such as using a linked list to provide the List API.
• When the implementation is changed, the contract would need to get changed as well, breaking the API.

Hiding implementation details

Another internal decision is the encoding of the empty list. In this example, we implement it as (*List)(nil). While this is an idiomatic choice in Go, we still exemplify how this can be hidden. Some functions like Head cannot be called with an empty list. The precondition l != nil would leak this to clients. Instead, we provide a pure method IsEmpty to be used in contracts.

// Returns the empty list.
// @ ensures l.Mem()
// @ ensures l.IsEmpty()
func Empty() (l *List) {
	l = (*List)(nil)
	// @ fold l.Mem()
	return
}

// Returns true iff the list is empty.
// @ pure
// @ requires l.Mem()
// @ decreases
func (l *List) IsEmpty() (empty bool) {
	return l == nil
}

// Head returns the value of the first element in the list.
// @ pure
// @ requires l.Mem()
// @ requires !l.IsEmpty()
// @ decreases
func (l *List) Head() (value int) {
	return /*@ unfolding l.Mem() in @*/ l.Value
}

func client() {
	e := Empty()
	// @ assert e.Mem()
	// @ assert e.IsEmpty()
	l1 := New(11, e)
	// @ assert l1.Mem()
	// @ assert l1.Head() == 11
	l2 := New(22, Empty())
	// @ assert l2.Head() == 22
	l3 := New(33, l2)
	// @ assert l3.Head() == 33
}

Note that we implement Mem such that it holds for the empty list as well. This enables us to call methods such as e.IsEmpty() on it.

List example so far

package list

type List struct {
	// Pointer to the next element in the linked list.
	next *List
	// The value stored with this element.
	Value int
}


/*@
// Represents access to the List element and all elements in its tail.
pred (l *List) Mem() {
	l != nil ==> (acc(l) && l.next.Mem())
}
@*/

// Returns the empty list.
// @ ensures l.Mem()
// @ ensures l.IsEmpty()
func Empty() (l *List) {
	l = (*List)(nil)
	// @ fold l.Mem()
	return
}


// New creates a new List node with the specified value and tail.
// @ requires tail.Mem()
// @ ensures out.Mem()
// @ ensures !out.IsEmpty()
// @ ensures out.Head() == value
func New(value int, tail *List) (out *List) {
	out = &List{next: tail, Value: value}
	// @ fold out.Mem()
	return
}


// Head returns the value of the first element in the list.
// @ pure
// @ requires l.Mem()
// @ requires !l.IsEmpty()
// @ decreases
func (l *List) Head() (value int) {
	return /*@ unfolding l.Mem() in @*/ l.Value
}


// Returns true iff the list is empty.
// @ pure
// @ requires l.Mem()
// @ decreases
func (l *List) IsEmpty() (empty bool) {
	return l == nil
}


func client() {
	e := Empty()
	// @ assert e.Mem()
	// @ assert e.IsEmpty()
	l1 := New(11, e)
	// @ assert l1.Mem()
	// @ assert l1.Head() == 11
	l2 := New(22, Empty())
	// @ assert l2.Head() == 22
	l3 := New(33, l2)
	// @ assert l3.Head() == 33
}

unfolding predicates

The unfolding P in E statement temporarily unfolds the predicate instance P in a pure expression E and folds it back.

For example, the pure function Head uses unfolding in its body to temporarily get permissions for l.Value:

// Head returns the value of the first element in the list.
// @ pure
// @ requires l.Mem()
// @ requires !l.IsEmpty()
// @ decreases
func (l *List) Head() (value int) {
	return /*@ unfolding l.Mem() in @*/ l.Value
}

Due to the syntactic restrictions of pure functions, there is no other way of using the fold and unfold statements.

Recall that the predicate instance l.Mem() is transferred back implicitly for the pure function.

Predicates and fractional permissions

Predicate instances are resources, i.e., permissions are used to track access to them. So far, we have been using l.Mem(), which is a shorthand for specifying a permission amount of 1 to the predicate instance l.Mem(). Equivalently, we can write acc(l.Mem()) or acc(l.Mem(), 1) using the access predicate.

For fold, unfold, and unfolding we may specify a permission amount p. In this case, any permission amount in the body of the predicate is multiplied by p. For example, the body of l.Mem() contains acc(l) and l.next.Mem(). After unfold acc(l.Mem()), only acc(l, 1/2) and acc(l.next.Mem(), 1/2) are held.

func fractional() {
	l := New(1, Empty())
	// @ assert l.Mem()
	// @ assert acc(l.Mem())
	// @ assert acc(l.Mem(), 1)

	// @ unfold acc(l.Mem(), 1/2)
	// @ assert acc(l.Mem(), 1/2)
	// @ assert acc(l, 1/2) && acc(l.next.Mem(), 1/2)
	// @ fold acc(l.Mem(), 1/2)
	// @ assert l.Mem()
}

List methods such as Head and Get do not need write permissions. Hence, we change their contracts to only require acc(l.Mem(), 1/2), and update any fold operations to use the correct permission amount. For methods like Remove that modify the List, we still require write access. For now, disregard l.View() in the contracts.

// Head returns the value of the first element in the list.
// @ pure
// @ requires acc(l.Mem(), 1/2)
// @ requires !l.IsEmpty()
// @ ensures value == l.View()[0]
// @ decreases
func (l *List) Head() (value int) {
	return /*@ unfolding acc(l.Mem(), 1/2) in @*/ l.Value
}

// Get returns the element at index i in the list.
// @ preserves acc(l.Mem(), 1/2)
// @ preserves 0 <= i && i < len(l.View())
// @ ensures value == l.View()[i]
// @ decreases l.Mem()
func (l *List) Get(i int) (value int) {
	// @ unfold acc(l.Mem(), 1/2)
	if i == 0 {
		value = l.Value
	} else {
		value = l.next.Get(i - 1)
	}
	// @ fold acc(l.Mem(), 1/2)
	return
}

// Remove returns the list with the element at index i deleted.
// @ requires l.Mem()
// @ requires 0 <= i && i < len(l.View())
// @ ensures out.Mem()
// @ ensures out.View() == old(l.View()[:i] ++ l.View()[i+1:])
func (l *List) Remove(i int) (out *List) {
	// @ unfold l.Mem()
	if i == 0 {
		return l.next
	}
	l.next = l.next.Remove(i - 1)
	// @ fold l.Mem()
	return l
}

Fractional permissions are crucial to frame properties. When retaining a positive permission amount across a call of Get, we know that the list is not modified. If write permissions were required, the contract would need to explicitly state that the list does not get modified.

For pointers, acc(x, 2) implies false. For predicates, we may have permission amounts larger than 1. For example, we can have acc(p2(l), 2), which denotes access to two predicate instances p2(l).

/*@
pred p2(l *List) {
	acc(&l.next, 1/2) && (l.next != nil ==> p2(l.next))
}
@*/

func client2() {
	l := &List{Value: 1, next: nil}
	// @ fold p2(l)
	// @ assert acc(p2(l), 1)
	// @ fold p2(l)
	// @ assert acc(p2(l), 2)
}

Abstraction functions

An idiomatic verification pattern is to map structures to their essential representation with an abstraction function. One way to specify functional correctness is by describing the effect of functions or methods on the abstract representation. For the abstract representation, we use mathematical types, i.e., ghost types representing mathematical objects, such as sequences or sets. For example, if we were to design a Set data structure, adding an element to a concrete Set shall have the same effect as the operation on an abstract, mathematical set.

Abstraction function for List

So far, our contracts for List were concerned with memory access. Now, we want to complete them with functional correctness requirements.

The essence of a List is captured by a sequence. We will not fully introduce sequences at this point, but refer the reader to the mathematical types reference if questions arise.

A sequence of integers seq[int] is constructed recursively from the list, concatenating (++) the sequences. By convention, the abstraction function is called View. Note that the function must be pure, as we want to use it in specifications.

ghost
pure
requires acc(l.Mem(), 1/2)
decreases l.Mem()
func (l *List) View() seq[int] {
	return l == nil ? seq[int]{} : unfolding acc(l.Mem(), 1/2) in seq[int]{l.Value} ++ l.next.View()
}

Functional correctness for List

For the methods of the List API, we can specify their functional behavior on the abstract object. For example, New corresponds to the concatenation of a single element to a sequence.

In the table, we give the preconditions and postconditions we add to the contracts. The abstraction function is heap dependent, and we can evaluate it in the old state to get the original representation. For example, the method Get must return the ith element of the sequence corresponding to the list old(l.View()[i]) index the index is within bounds ( 0 <= i && i < len(l.View())).

The full example can be found here: full linked list example.

Predicates as termination measures

Predicate instances can be used as termination measures. The measure decreases if an instance is nested within another predicate instance. For example, l1.Mem() is nested within l2.Mem() and l2.Mem() is nested within l3.Mem().

l1 := New(1, Empty())
// @ fold l1.Mem()
l2 := New(2, l1)
// @ fold l2.Mem()
l3 := New(3, l2)
// @ fold l3.Mem()

The termination measure is lower bounded for predicate instances with a finite unfolding ¹. For example, l3.Mem() has two predicate instances nested within, whereas l1.Mem() has no other predicate instance nested within.

To prove termination of the List method Length, we add the termination measure l.Mem(). As is common for recursive functions, we unfold the predicate instance before the recursive call. It is decreasing since l.next.Mem() is nested within l.Mem().

// Returns the length of the list.
// @ preserves acc(l.Mem(), 1/2)
// @ ensures length == len(l.View())
// @ decreases l.Mem()
func (l *List) Length() (length int) {
	if l == nil {
		return 0
	} else {
		// @ unfold acc(l.Mem(), 1/2)
		length = 1 + l.next.Length()
		// @ fold acc(l.Mem(), 1/2)
		return length
	}
}

Please note that we write decreases l.Mem() instead of decreases acc(l.Mem(), 1/2), even if we only require acc(l.Mem(), 1/2).

For the List API, we can use the termination measure l.Mem() for the methods Length , Get, View.

It might be tempting to use the length of a List or the length of the sequence from the abstraction function View as an integer termination measure. For this, the function must be pure, which requires a termination measure in turn.

We chose a recursive implementation for Length, in order to preserve access to l.Mem(). An idiomatic iterative implementation is more challenging to verify. When iteratively iterating over a list, we keep unfolding current.Mem() and lose access to the already visited elements. It is not directly clear how one could fold the predicate instances back such that l.Mem() is preserved by LengthIterative. A common approach is to define a predicate that denotes access to a segment of a list instead of the entire tail. Alternatively, magic wands are applicable in this situation.

// @ requires l.Mem()
// @ decreases l.Mem()
func (l *List) LengthIterative() (length int) {
	current := l
	// @ invariant current.Mem()
	// @ decreases current.Mem()
	for current != nil {
		// @ unfold current.Mem()
		length += 1
		current = current.next
	}
	return
}

/*@
pred stream(l *List) {
	acc(l) && stream(l.next)
}
@*/

// @ requires stream(l)
// @ decreases
func streaming(l *List) {
	a := 0
	// @ invariant stream(l)
	// @ decreases stream(l)
	for {
		// @ unfold stream(l)
		a += l.Value
		l = l.next
	}
}

Full linked list example

package list

type List struct {
	// Pointer to the next element in the linked list.
	next *List
	// The value stored with this element.
	Value int
}


/*@
// Represents access to the List element and all elements in its tail.
pred (l *List) Mem() {
	l != nil ==> (acc(l) && l.next.Mem())
}
@*/

// Returns the empty list.
// @ ensures l.Mem()
// @ ensures l.IsEmpty()
func Empty() (l *List) {
	l = (*List)(nil)
	// @ fold l.Mem()
	return
}

// New creates a new List node with the specified value and tail.
// @ requires tail.Mem()
// @ ensures out.Mem()
// @ ensures out.View() == seq[int]{value} ++ old(tail.View())
func New(value int, tail *List) (out *List) {
	out = &List{next: tail, Value: value}
	// @ fold out.Mem()
	return
}


// Tail returns a new list that is the tail of the original list,
// excluding the first element.
// @ requires l.Mem()
// @ requires !l.IsEmpty()
// @ ensures out.Mem()
// @ ensures out.View() == old(l.View()[1:])
func (l *List) Tail() (out *List) {
	// @ unfold l.Mem()
	out = l.next
	return
}

// Remove returns the list with the element at index i deleted.
// @ requires l.Mem()
// @ requires 0 <= i && i < len(l.View())
// @ ensures out.Mem()
// @ ensures out.View() == old(l.View()[:i] ++ l.View()[i+1:])
func (l *List) Remove(i int) (out *List) {
	// @ unfold l.Mem()
	if i == 0 {
		return l.next
	}
	l.next = l.next.Remove(i - 1)
	// @ fold l.Mem()
	return l
}


// Head returns the value of the first element in the list.
// @ pure
// @ requires acc(l.Mem(), 1/2)
// @ requires !l.IsEmpty()
// @ ensures value == l.View()[0]
// @ decreases
func (l *List) Head() (value int) {
	return /*@ unfolding acc(l.Mem(), 1/2) in @*/ l.Value
}


// Get returns the element at index i in the list.
// @ preserves acc(l.Mem(), 1/2)
// @ preserves 0 <= i && i < len(l.View())
// @ ensures value == l.View()[i]
// @ decreases l.Mem()
func (l *List) Get(i int) (value int) {
	// @ unfold acc(l.Mem(), 1/2)
	if i == 0 {
		value = l.Value
	} else {
		value = l.next.Get(i - 1)
	}
	// @ fold acc(l.Mem(), 1/2)
	return
}


// Returns true iff the list is empty.
// @ pure
// @ requires acc(l.Mem(), 1/2)
// @ ensures empty == (len(l.View()) == 0)
// @ decreases
func (l *List) IsEmpty() (empty bool) {
	return l == nil
}


// Returns the length of the list.
// @ preserves acc(l.Mem(), 1/2)
// @ ensures length == len(l.View())
// @ decreases l.Mem()
func (l *List) Length() (length int) {
	if l == nil {
		return 0
	} else {
		// @ unfold acc(l.Mem(), 1/2)
		length = 1 + l.next.Length()
		// @ fold acc(l.Mem(), 1/2)
		return length
	}
}


/*@
ghost
pure
requires acc(l.Mem(), 1/2)
decreases l.Mem()
func (l *List) View() seq[int] {
	return l == nil ? seq[int]{} : unfolding acc(l.Mem(), 1/2) in seq[int]{l.Value} ++ l.next.View()
}
@*/

func client() {
	ll := Empty()
	l0 := ll.Length()
	// @ assert l0 == 0
	ll = New(11, ll)
	// @ assert ll.Mem()
	// @ assert ll.Head() == 11
	// @ assert ll.View() == seq[int]{11}
	l1 := ll.Length()
	// @ assert l1 == 1
	ll = ll.Tail()
	// @ assert ll.View() == seq[int]{}
	ll = New(22, Empty())
	// @ assert ll.Head() == 22
	ll = New(33, ll)
	// @ assert ll.Head() == 33
	l2 := ll.Length()
	// @ assert l2 == 2
	v0 := ll.Get(0)
	v1 := ll.Get(1)
	// @ assert v0 == 33
	// @ assert v1 == 22
	ll := ll.Remove(1)
	l3 := ll.Length()
	// @ assert ll.Head() == 33
	// @ assert l3 == 1
}

Triggers

TODO

Please refer to the Viper tutorial for now:

https://viper.ethz.ch/tutorial/#quantifiers

Magic Wands

TODO

Please refer to the Viper tutorial for now: https://viper.ethz.ch/tutorial/#magic-wands

Mathematical types (seq, set, mset, dict)

This section gives an overview of the mathematical types supported by Gobra and their operations. Examples illustrate the syntax and the operations.

Note that mathematical types are ghost types and may only be used in ghost code.

Sequences (seq)

The type seq[T] represents finite sequences with elements of type T.

Example: seq[int]

	// The empty sequence
	empty := seq[int]{}
	// Length of the sequence
	assert len(empty) == 0
	// Constructing from a literal
	s := seq[int]{0, 1, 1, 2, 3}
	// Membership check
	assert 1 in s && !(4 in s)
	// Lookup
	assert s[4] == 3
	// Integer sequence shorthand
	s1 := seq[0..5]
	// Comparison
	assert seq[0..5] == seq[int]{0, 1, 2, 3, 4}
	// Works also with other integer types such as byte
	assert seq[0..2] == seq[byte]{byte(0), byte(1)}
	assert seq[4..2] == seq[int]{}
	s2 := seq[5..10]
	s3 := seq[0..10]
	// Concatentation of sequences with ++
	assert s1 ++ s2 == s3
	// Subsequences
	assert s3[0:5] == s1
	// Omitting the first index
	assert s3[:5] == s1
	// Omitting both indices
	assert s3[:] == s3
	// No well-defined requirements for sub-sequence indices
	assert len(s3[5:1]) == 0
	assert len(s3[-10:20]) == 10
	// Conversion from an array
	arr := [5]int{0, 1, 2, 3, 4}
	s4 := seq(arr)
	// Conversion from another sequence
	assert s4 == seq(s4)
	s5 := seq[int]{0, 0, 0}
	// Create from sequence with update
	s6 := s5[0 = 2]
	// The original sequence is not modified (it is immutable)
	assert s6[0] == 2 && s5[0] == 0
	assert s5[0 = 2][1 = 4][2 = 8] == seq[int]{2, 4, 8}

Sets (set)

The type set[T] represents mathematical sets with elements of type T.

Example: set[int]

	// The empty set
	empty := seq[int]{}
	s1 := set[int]{1, 2, 3}
	s2 := set[int]{1, 2, 2, 3, 3, 3}
	// Equality
	assert s1 == s2
	// Cardinality
	assert len(s1) == len(s2)
	// Conversion from a sequence
	s3 := set(seq[int]{ 1, 2})
	// Conversion from a set
	s4 := set(s1)
	// Membership
	assert 1 in set[int]{1, 2} && !(0 in set[int]{1, 2})
	// Set operations
	assert set[int]{0, 2} subset set[int]{0, 1, 2}
	assert set[int]{0, 2} union set[int]{1} == set[int]{0, 1, 2}
	assert set[int]{0, 1} intersection set[int]{1, 2} == set[int]{1}
	assert set[int]{0, 1} setminus set[int]{1, 2} == set[int]{0}

Multisets (mset)

The type mset[T] represents multisets with elements of type T. Multisets are like sets but may contain the same element multiple times. The multiset operations respect the multiplicities of the elements.

Example: mset[int]

	m1 := mset[int]{1, 2, 3}
	m2 := mset[int]{1, 2, 2, 3, 3, 3}
	assert len(m1) == 3 && len(m2) == 6
	// Multiplicity
	assert 3 # m1 == 1 && 3 # m2 == 3
	assert 4 # m1 == 0
	// multiset operations
	assert mset[int]{0, 1} union mset[int]{1} == mset[int]{0, 1, 1}
	assert mset[int]{1, 1, 1} intersection mset[int]{1, 1, 2} == mset[int]{1, 1}
	assert mset[int]{1, 1, 2} setminus mset[int]{1, 2, 2} == mset[int]{1}
	assert mset[int]{1} subset mset[int]{1, 1}
	assert !(mset[int]{1, 1} subset mset[int]{1})

Dictionaries (dict)

The type dict[K]V represents dictionaries with keys of type K and values of type V.

m1 := dict[string]int{ "one": 1, "two": 2, "one": -1}

ERROR key appears twice in map literal
    m1 := dict[string]int{ "one": 1, "two": 2, "one": -1}
    ^

m1 := dict[string]int{ "one": 1, "two": 2}
assert m1["three"] == 3

ERROR Assert might fail. 
Key "three" might not be contained in m1.

Example: dict[string]int

	m1 := dict[string]int{ "one": 1, "two": 2}
	assert m1["one"] == 1
	assert len(m1) == 2
	assert domain(m1) == set[string]{"one", "two"}
	assert range(m1) == set[int]{1, 2}
	// update dict
	m2 := m1["three" = 3, "four" = 4]
	// syntactic sugar for
	m2 = m2["zwei" = 2]
	m2["zwei"] = 2
	assert m2["zwei"] == 2 && m2["three"] == 3 && m2["four"] == 4