Overview

🚧 This book is under construction. It is very incomplete at the moment and it is likely to change significantly. 🚧

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.

Overflow checking is still experimental and under implementation, and because of that, it is disabled by default. It can be enabled with the option --overflow in the CLI, or with the annotation // ##(--overflow) in the beginning of a file.

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() {}

is equivalent to

// @ requires true
// @ ensures true
func foo() {}

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.

func client1() int {
	a := [5]int{2, 3, 5, 7, 11}
	b1 := a[-1] // invalid index (too small)
	b2 := a[1]  // valid index
	b3 := a[10] // invalid index (too large)
	return b1 + b2 + b3
}

./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:

func readArr(a [5]int, i int) int {
	b := a[i]
	return b
}

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

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.readArr(...)
        /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 readArr, Gobra accepts the function.

func readArr(a [5]int, i int) int {
	b := a[i]
	return b
}

Then the calls readArr(a, -1) and readArr(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

While we include triggers in the following examples as a best practice, readers may disregard them for now. Choosing the right trigger expressions may require careful consideration. This advanced topic will be addressed in the section on triggers.

Existential quantifier `exists`

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

Existential quantifiers tend to lead to slow and unpredictable verification times. As such, we recommend using them sparingly. Later, we show how we might avoid having to use explicit existential quantifiers through the introduction of ghost state.

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.

In practice, we may not want to write such a function, as the array must be copied every time we call this function - after all, arrays are passed by value. On another note: the contract of sort only specifies that the returned array is sorted. An implementation returning an array full of zeros adheres to this contract. To properly specify sort, one should include a postcondition stating that the multiset of elements in the returned array is the same as the multiset of elements of the array passed to the function.

In Gobra the operator for the implication if P then Q is P ==> Q. It has the following truth table:

`P ==> Q`	`Q=false`	`Q=true`
`P=false`	1	1
`P=true`	0	1

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

before the first iteration after performing the initialization statement
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:

We initialize i := 0, so the invariant holds before the first loop iteration.
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

before the first iteration after performing the initialization statement

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}
	BinarySearchArr(arr, 2)   // 3 true
	BinarySearchArr(arr, 4)   // 5 false
	BinarySearchArr(arr, -1)  // 0 false
	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:

Before the first iteration mid is initialized to 0. Therefore, 0 <= mid && mid < N trivially holds.
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:

`low`	`high`	`arr[:low]`	`arr[low:high]`	`arr[high:]`
0	7	[]	[0 1 1 2 3 5 8]	[]
4	7	[0 1 1 2]	[3 5 8]	[]
4	5	[0 1 1 2]	[3 5]	[8]
5	5	[0 1 1 2 3]	[]	[5 8]

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:

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.
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 {
		mid = (low + high) / 2
		if arr[mid] < target {
			low = mid + 1
		} else {
			high = mid
		}
	}
	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

Overflow checking is still an experimental feature under development. You may encounter bugs and observe unexpected results.

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
}

ERROR expected pure expression, but got '8 ==  Cube(3)'
    assert 8 == Cube(3)
        ^
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) { // error
    if n <= 1 {
        return n
    } else {
        return fibonacci(n-1) + fibonacci(n-2)
    }
}

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

We saw that we can replace the call of a pure function with its body.
Divide both sides by incons(1) (without the precondition ensures res != 0, Gobra reports the error Divisor incons(1) might be zero.)
Arithmetic
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).

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
}

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)

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.

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}
}

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).

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).

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

checks that all value constraints in ASSERTION hold, otherwise an error is reported.
checks that all permissions mentioned by ASSERTION are held, otherwise an error is reported.
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

adds all permissions mentioned by ASSERTION
assumes all value constraints in ASSERTION hold

Inhaling can result in an inconsistent state. Do not use it without a good reason, except for debugging and learning.

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)

Can access predicates occur within the body of the exists quantifier? The short answer is no. Consider the hypothetical precondition requires exists i int :: acc(&s[i]). This is not helpful because it would provide access to some element of the slice s, but we cannot determine which element, as Gobra does not provide an instance of i.

Recursive data structures, such as a linked list, can also introduce an unbounded number of locations. In chapter 3 we explore how recursive predicates can be used in this case.

Pure functions and permissions

Recall that pure functions have no side effects. Hence, they must not leak any permissions and implicitly transfer back 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. It is idiomatic to use wildcard permissions since all the permissions held before a pure function call are still held after the call.

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 acc(xs, 1)
    // @ assert allZero(xs)
    // @ assert acc(xs, 1)
}

Pure functions do not leak any permissions.

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) @*/)
// 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 {
		mid = (low + high) / 2
		if s[mid] < target {
			low = mid + 1
		} else {
			high = mid
		}
	}
	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.

https://go.dev/ref/spec#For_range

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
}

Declaring 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.

Creating predicate instances 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 predicate instances 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.

Go's standard library comes with a doubly linked list. While it has been verified (Verifying Go’s Standard Library (Jenny)), we use a much simpler API for our exposition.

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())).

name	`requires`	`ensures`
`New`		`out.View() == seq[int]{value} ++ old(tail.View())`
`Tail`		`out.View() == old(l.View()[1:])`
`Remove`	`0 <= i && i < len(l.View())`	`out.View() == old(l.View()[:i] ++ l.View()[i+1:])`
`Head`		`value == l.View()[0]`
`Get`	`0 <= i && i < len(l.View())`	`value == l.View()[i]`
`IsEmpty`		`empty == (len(l.View()) == 0)`
`Length`		`length == 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
}

Technically, a predicate instance with no finite unfolding is still accepted as a termination measure by Gobra. For example, the recursive predicate stream represents access to an infinite list, and a predicate instance stream(l) has no finite unfolding. Nevertheless, it can be used as a termination measure, with the unexpected behavior that we can prove that streaming terminates.

/*@
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
}

Behavioral subtypes

Interfaces in Go are defined as a set of method signatures. In Gobra, we can add signatures and contracts to the interface definitions. It must be proven that the implementation is a behavioral subtype of the interface, i.e., it provides not only at least the same methods, but also at least the same behavior:

The precondition of each interface method must imply the precondition of each corresponding implementation method
The postcondition of each implementation method must imply the postcondition of each corresponding interface method.

In this section, we look at interfaces from the image package from the Go standard library. As a first example, we consider the Color interface with a single method RGBA that returns color components for red, green, blue, and alpha.

// Color can convert itself to alpha-premultiplied 16-bits per channel RGBA.
// The conversion may be lossy.
type Color interface {
	// Returns true if the implementation holds a valid color.
	// @ ghost
	// @ pure
	// @ decreases
	// @ Valid() bool

	// RGBA returns the alpha-premultiplied red, green, blue and alpha values
	// for the color. Each value ranges within [0, 0xffff], but is represented
	// by a uint32 so that multiplying by a blend factor up to 0xffff will not
	// overflow.
	//
	// An alpha-premultiplied color component c has been scaled by alpha (a),
	// so has valid values 0 <= c <= a.
	// @ preserves Valid()
	// @ ensures 0 <= r && r <= a && 0 <= g && g <= a && 0 <= b && b <= a && a <= 0xffff
	RGBA() (r, g, b, a uint32)
}

// source: https://cs.opensource.google/go/go/+/refs/tags/go1.24.0:src/image/color/color.go;l=10

We add a contract to the signature that formalizes the docstring, which states that each value falls within the range [0, 0xffff] and "an alpha-premultiplied color component c has been scaled by alpha (a), so has valid values 0 <= c <= a." Furthermore, we add a ghost and pure method Valid to the interface. With Valid, implementations provide an assertion that must hold for the data structure such that a valid color can be returned.

The type Alpha16, which represents a 16-bit alpha color:

// Alpha16 represents a 16-bit alpha color.
type Alpha16 struct {
	A uint16
}

// @ preserves c.Valid()
// @ ensures 0 <= r && r <= a && 0 <= g && g <= a && 0 <= b && b <= a && a <= 0xffff
func (c Alpha16) RGBA() (r, g, b, a uint32) {
	a = uint32(c.A)
	return a, a, a, a
}

In Go, interface implementation is implicit, i.e., the Color interface is implemented by defining an RGBA method. For Gobra, any ghost methods such as Valid must be implemented as well.

/*@
ghost
decreases
pure func (c Alpha16) Valid() bool {
	return 0 <= c.A && c.A <= 0xffff
}
@*/

Gobra checks that Alpha16 is a behavioral subtype of Color only when needed, that is, when an value of interface type has Alpha16 as its underlying type. For example, this occurs when we assign a value to a variable of interface type or pass an argument to a function with an in-parameter of interface type.

The following client verifies since the postcondition of Alpha16's RGBA is equivalent to the postcondition of the interface method.

func client1Alpha() {
	var c Color
	c = Alpha16{0xffff}
	r, _, _, a := c.RGBA()
	// @ assert 0 <= a && r <= a
}

The implementation's postcondition may be stronger. For example, the Constant color guarantees that it always returns the same color components. From this, the postcondition of the interface immediately follows.

type Constant struct{}

// @ ensures r == 0x0 && g == 0xffff && b == 0xffff && a == 0xffff
func (c Constant) RGBA() (r, g, b, a uint32) {
	return 0x0, 0xffff, 0xffff, 0xffff
}

/*@
ghost
decreases
pure func (c Constant) Valid() bool {
	return true
}
@*/

func client1Constant() {
	var c Color
	c = Constant{}
	r, _, _, a := c.RGBA()
	// @ assert 0 <= a && r <= a
}

Similarly, the implementation's precondition may be weaker.

Implementation precondition too strong

Gobra reports an error if the precondition of an implementation method might not follow from the precondition of the corresponding interface method.

In the following example, acc(c.p) is required to call RGBA with receivers of type Fail1. The function client has a parameter of interface type, whose concrete type is unknown. When c.RGBA() is called, the precondition of the interface method must hold. However, this does not imply the precondition of Fail1's RGBA. Hence, it would be unsound to allow Fail1 to be used as a value of type Color.

type Fail1 struct {
	p *uint32
}

// @ requires acc(c.p)
// @ requires c.Valid()
// @ ensures r <= 0xffff && g <= 0xffff && b <= 0xffff && a <= 0xffff
func (c Fail1) RGBA() (r, g, b, a uint32) {
	a = *c.p
	return a, a, a, a
}

/*@
ghost
requires acc(c.p)
decreases
pure func (c Fail1) Valid() bool {
	return 0 <= *c.p && *c.p <= 0xffff
}
@*/

func client2(c Color) {
	c = Fail1{new(uint32)}
	r, _, _, a := c.RGBA()
	// @ assert 0 <= a && r <= a
}

ERROR Generated implementation proof (Fail1 implements interface{ RGBA }) failed. Precondition of call to implementation method might not hold. 
Permission to c.p might not suffice.

ERROR Precondition of call c.RGBA() might not hold. 
Assertion Valid() might not hold.

Implementation postcondition too weak

An error is reported if the postcondition of an implementation method might not imply the postcondition of the corresponding interface method.

type Fail2 struct{}

// @ ensures 0 <= r && r <= a && 0 <= g && g <= a && 0 <= b && b <= a
// @ ensures c.Valid()
func (c Fail2) RGBA() (r, g, b, a uint32) {
	return 255, 255, 255, 255
}

/*@
ghost
decreases
pure func (c Fail2) Valid() bool {
	return true
}
@*/

func client3() {
	var c Color
	c = Fail2{}
}

ERROR Generated implementation proof (Fail2 implements interface{ RGBA }) failed. Postcondition of interface method might not hold. 

Assertion a <= 0xffff might not hold.

In the above example, the postcondition a <= 0xffff is missing from the contract of the implementation. It does not follow from the given postcondition:

// @ ensures 0 <= r && r <= a && 0 <= g && g <= a && 0 <= b && b <= a

So far, we have relied on generated implementation proofs from Gobra. In a following section, we show how to provide our own implementation proofs.

The precondition of the interface method must imply the precondition of the implementation method.

The postcondition of the implementation method must imply the postcondition of the interface method.

Full section example

package main

// Color can convert itself to alpha-premultiplied 16-bits per channel RGBA.
// The conversion may be lossy.
type Color interface {
	// Returns true if the implementation holds a valid color.
	// @ ghost
	// @ pure
	// @ decreases
	// @ Valid() bool

	// RGBA returns the alpha-premultiplied red, green, blue and alpha values
	// for the color. Each value ranges within [0, 0xffff], but is represented
	// by a uint32 so that multiplying by a blend factor up to 0xffff will not
	// overflow.
	//
	// An alpha-premultiplied color component c has been scaled by alpha (a),
	// so has valid values 0 <= c <= a.
	// @ preserves Valid()
	// @ ensures 0 <= r && r <= a && 0 <= g && g <= a && 0 <= b && b <= a && a <= 0xffff
	RGBA() (r, g, b, a uint32)
}

// source: https://cs.opensource.google/go/go/+/refs/tags/go1.24.0:src/image/color/color.go;l=10

// Alpha16 represents a 16-bit alpha color.
type Alpha16 struct {
	A uint16
}

// @ preserves c.Valid()
// @ ensures 0 <= r && r <= a && 0 <= g && g <= a && 0 <= b && b <= a && a <= 0xffff
func (c Alpha16) RGBA() (r, g, b, a uint32) {
	a = uint32(c.A)
	return a, a, a, a
}


/*@
ghost
decreases
pure func (c Alpha16) Valid() bool {
	return 0 <= c.A && c.A <= 0xffff
}
@*/

func client1Alpha() {
	var c Color
	c = Alpha16{0xffff}
	r, _, _, a := c.RGBA()
	// @ assert 0 <= a && r <= a
}


type Constant struct{}

// @ ensures r == 0x0 && g == 0xffff && b == 0xffff && a == 0xffff
func (c Constant) RGBA() (r, g, b, a uint32) {
	return 0x0, 0xffff, 0xffff, 0xffff
}

/*@
ghost
decreases
pure func (c Constant) Valid() bool {
	return true
}
@*/

func client1Constant() {
	var c Color
	c = Constant{}
	r, _, _, a := c.RGBA()
	// @ assert 0 <= a && r <= a
}

`nil` interface values

A nil interface value holds neither a value nor a concrete type [1]. For example, the variable c of type Color is not assigned a concrete value.

// without specifications for simplicity
type Color interface {
	RGBA() (r, g, b, a uint32)
}

func main() {
	var c Color
	// @ assert c == nil
	client1(c)
}

func client1(c Color) {
	c.RGBA() // error
}

Go panics with a run-time error if a method is called on a nil interface value. Since it holds no concrete type, there is no way to look up which concrete RGBA method to call.

panic: runtime error: invalid memory address or nil pointer dereference

Gobra statically reports an error instead:

ERROR Precondition of call c.RGBA() might not hold. 

The receiver might be nil

Note that an interface variable holding a concrete type is non-nil, even when the concrete value is nil. In the following example, *SomeColor implements the interface Color. The first two assertions pass since c has the dynamic type *SomeColor. Hence, calling the method RGBA is legal. Since the receiver (s *SomeColor) might be nil, the last assertion fails:

func client2() {
	var c Color = (*SomeColor)(nil)
	// @ assert c != nil
	// @ assert typeOf(c) == type[*SomeColor]
	c.RGBA()
}

type SomeColor struct{ x int }

func (s *SomeColor) RGBA() (r, g, b, a uint32) {
	// @ assert s != nil // error
	a = uint32(s.x)
	return a, a, a, a
}

ERROR Assert might fail.

Assertion s != nil might not hold.

Full section example

Gobra is expected to find 2 errors.

package main

// without specifications for simplicity
type Color interface {
	RGBA() (r, g, b, a uint32)
}

func main() {
	var c Color
	// @ assert c == nil
	client1(c)
}

func client1(c Color) {
	c.RGBA() // error
}


func client2() {
	var c Color = (*SomeColor)(nil)
	// @ assert c != nil
	// @ assert typeOf(c) == type[*SomeColor]
	c.RGBA()
}

type SomeColor struct{ x int }

func (s *SomeColor) RGBA() (r, g, b, a uint32) {
	// @ assert s != nil // error
	a = uint32(s.x)
	return a, a, a, a
}

Type assertions, `typeOf`

Another interface from the image package of the Go standard library is the Model, to convert between different color models. In this section, we study an implementation of this interface using both type assertions and the typeOf function from Gobra.

// Model can convert any [Color] to one from its own color model. The conversion
// may be lossy.
type Model interface {
	// @ requires c != nil
	// @ ensures res != nil
	Convert(c Color) (res Color)
}

// without specifications for simplicity
type Color interface {
	RGBA() (r, g, b, a uint32)
}

We cannot convert any color as described in the docstring, but any color with c != nil to exclude the case of the nil interface value.

Type assertions

Given an interface value v of underlying type T, we can recover the concrete value i of type T using a type assertion i := v.(T). This operation might cause a run-time panic when the underlying type is not T. In the following example, Gobra reports an error since the underlying type of the variable c is unknown:

// @ requires c != nil
func TypeAssertion(c Color) {
	c1 := c.(Alpha16) // error
	r, g, b, a := c1.RGBA()
	// @ assert r == g
}

ERROR Type assertion might fail. 

Dynamic value might not be a subtype of the target type.

By assigning a second variable i, ok := v.(T), the type assertion no longer panics. If ok is true then i is the underlying value. Otherwise if ok is false, i is the zero value of type T [1].

As an example, consider the implementation of the Model interface for the alpha16Model, which converts a color to the Alpha16 color model. By using a type assertion, we can return the argument if it is already an Alpha16 color:

type alpha16Model struct{}

var Alpha16Model alpha16Model

// @ requires c != nil
// @ ensures res != nil
// @ ensures typeOf(res) == type[Alpha16]
func (_ alpha16Model) Convert(c Color) (res Color) {
	if _, ok := c.(Alpha16); ok {
		return c
	}
	_, _, _, a := c.RGBA()
	return Alpha16{uint16(a)}
}

Dynamic types with `typeOf`

Gobra provides the typeOf function, which takes an argument of an interface value and returns its dynamic type. In the example above, we specified in the Convert implementation of alpha16Model that the return type is Alpha16. Note that to implement the Model interface, the return type must be Color, not Alpha16.

// @ ensures typeOf(res) == type[Alpha16]

We must wrap the type T with type[T] to refer to it. With this postcondition, the following client code verifies:

func converting() {
	c1 := Constant{}
	c2 := Alpha16Model.Convert(c1)
	c3 := c2.(Alpha16)
	c3.RGBA()
}

Full section example

package main

// without specifications for simplicity
type Color interface {
	RGBA() (r, g, b, a uint32)
}


type Alpha16 struct {
	A uint16
}

type Constant struct{}

// @ ensures r == 0x0 && g == 0xffff && b == 0xffff && a == 0xffff
func (c Constant) RGBA() (r, g, b, a uint32) {
	return 0x0, 0xffff, 0xffff, 0xffff
}

func (c Alpha16) RGBA() (r, g, b, a uint32) {
	a = uint32(c.A)
	return a, a, a, a
}


// Model can convert any [Color] to one from its own color model. The conversion
// may be lossy.
type Model interface {
	// @ requires c != nil
	// @ ensures res != nil
	Convert(c Color) (res Color)
}


func converting() {
	c1 := Constant{}
	c2 := Alpha16Model.Convert(c1)
	c3 := c2.(Alpha16)
	c3.RGBA()
}


type alpha16Model struct{}

var Alpha16Model alpha16Model

// @ requires c != nil
// @ ensures res != nil
// @ ensures typeOf(res) == type[Alpha16]
func (_ alpha16Model) Convert(c Color) (res Color) {
	if _, ok := c.(Alpha16); ok {
		return c
	}
	_, _, _, a := c.RGBA()
	return Alpha16{uint16(a)}
}

// @ alpha16Model implements Model

Abstracting memory with predicate interface members

In Gobra we can include predicate signatures within an interface. This feature is particularly significant for abstracting memory, as interfaces define methods rather than fields, so we cannot specify access to concrete fields. Each implementation must define its own predicate to abstract memory access. Consequently, an interface can specify required behaviors without imposing constraints on the underlying data representation.

As an example, we consider the Image interface from the Go standard library. It includes methods to retrieve the color Model (which itself is an interface) as well as a method to obtain a valid Color (also an interface) for a given pixel at coordinates (x, y).

The predicate Mem represents memory access and the ghost and pure function Inv represents an invariant that holds for the data structure storing the image.

// Image is a finite rectangular grid of [Color] values taken from a color
// model.
type Image interface {
	// Mem represents the access to the memory of the Image
	// @ pred Mem()	// <----- Predicate member

	// Invariant that holds for valid images
	// @ ghost
	// @ pure
	// @ requires acc(Mem(), _)
	// @ decreases
	// @ Inv() bool

	// ColorModel returns the Image's color model.
	ColorModel() Model

	// Bounds returns the domain for which At can return non-zero color.
	// The bounds do not necessarily contain the point (0, 0).
	// @ requires acc(Mem(), _)
	// @ pure
	// @ decreases
	Bounds() (r Rectangle)

	// At returns the color of the pixel at (x, y).
	// At(Bounds().Min.X, Bounds().Min.Y) returns the upper-left pixel of the grid.
	// At(Bounds().Max.X-1, Bounds().Max.Y-1) returns the lower-right one.
	// @ preserves acc(Mem(), 1/2)
	// @ preserves Inv()
	// @ ensures c != nil && c.Valid()
	// @ ensures !Point{x, y}.In(Bounds()) ==> (c.RGBASpec() == rgba{})
	At(x, y int) (c Color)
}

// A Point is an X, Y coordinate pair. The axes increase right and down.
type Point struct {
	X, Y int
}

// In reports whether p is in r.
// @ pure
// @ decreases
func (p Point) In(r Rectangle) (res bool) {
	return r.Min.X <= p.X && p.X < r.Max.X &&
		r.Min.Y <= p.Y && p.Y < r.Max.Y
}

// A Rectangle contains the points with Min.X <= X < Max.X, Min.Y <= Y < Max.Y.
// It is well-formed if Min.X <= Max.X and likewise for Y. Points are always
// well-formed. A rectangle's methods always return well-formed outputs for
// well-formed inputs.
//
// A Rectangle is also an [Image] whose bounds are the rectangle itself. At
// returns color.Opaque for points in the rectangle and color.Transparent
// otherwise.
type Rectangle struct {
	Min, Max Point
}

Additionally, the boundaries of an image are encapsulated within a Rectangle struct, retrievable with the Bounds method. For points not contained in this rectangle, At must return zero color. We define zero color in terms of the RGBA method, or more precisely the corresponding pure and ghost method RGBASpec. Since pure methods must have exactly one parameter, we cannot return r, g, b, a. Instead, we define the ghost type rgba. So, rgba{} represents the zero color.

/*@
ghost type rgba ghost struct {
	r, g, b, a uint32
}

ghost
pure
decreases
func (c rgba) ColorRange() bool {
	return 0 <= c.r && c.r <= c.a && 0 <= c.g && c.g <= c.a &&
		0 <= c.b && c.b <= c.a && c.a <= 0xffff
}
@*/

// Color can convert itself to alpha-premultiplied 16-bits per channel RGBA.
// The conversion may be lossy.
type Color interface {
	// Returns true if the implementation holds a valid color.
	// @ ghost
	// @ pure
	// @ decreases
	// @ Valid() bool

	// @ ghost
	// @ requires Valid()
	// @ ensures c.ColorRange()
	// @ pure
	// @ decreases
	// @ RGBASpec() (ghost c rgba)

	// RGBA returns the alpha-premultiplied red, green, blue and alpha values
	// for the color. Each value ranges within [0, 0xffff], but is represented
	// by a uint32 so that multiplying by a blend factor up to 0xffff will not
	// overflow.
	//
	// An alpha-premultiplied color component c has been scaled by alpha (a),
	// so has valid values 0 <= c <= a.
	// @ preserves Valid()
	// @ ensures RGBASpec() == rgba{r, g, b, a}
	RGBA() (r, g, b, a uint32)
}

The type *Alpha16Image implements the Image interface. To implement the interface any predicates defined for the interface must be implemented. Here, the Mem predicate's body contains access to all fields of the struct, especially the elements of the Pix slice holding the image's pixel values.


// Alpha16Image is an in-memory image whose At method returns [color.Alpha16] values.
type Alpha16Image struct {
	// Pix holds the image's pixels, as alpha values in big-endian format. The pixel at
	// (x, y) starts at Pix[(y-Rect.Min.Y)*Stride + (x-Rect.Min.X)*2].
	Pix []uint8
	// Stride is the Pix stride (in bytes) between vertically adjacent pixels.
	Stride int
	// Rect is the image's bounds.
	Rect Rectangle
}

/*@
pred (p *Alpha16Image) Mem() {
	acc(p) && forall i int :: {&p.Pix[i]} 0 <= i && i < len(p.Pix) ==> acc(&p.Pix[i])
}
@*/

The pure and ghost function Inv represents an invariant that has to hold for the image. This invariant states that the entire entire size of the pixel slice is given by the stride times the height of the image: p.Stride*(p.Rect.Max.Y-p.Rect.Min.Y) == len(p.Pix), where the stride is the distance in bytes between vertically adjacent pixels. Note that the factor 2 in p.Stride == 2*(p.Rect.Max.X-p.Rect.Min.X) is due to the fact that each pixel uses 2 elements of the Pix slice for storage. Additionally, the elements of the pixel slice are of type uint8, so they have values in the range from 0 to 0xff. While this could be inferred from the type alone, we have to state this due to a current limitation in Gobra.

/*@
ghost
requires acc(p.Mem(), _)
pure
decreases
func (p *Alpha16Image) Inv() bool {
	return unfolding acc(p.Mem(), _) in (2*(p.Rect.Max.X-p.Rect.Min.X) == p.Stride &&
    	p.Stride * (p.Rect.Max.Y-p.Rect.Min.Y) == len(p.Pix)) &&
    	forall i int :: {&p.Pix[i]} 0 <= i && i < len(p.Pix) ==> 0 <= p.Pix[i] && p.Pix[i] <= 0xff
}
@*/

Please note that the annotations of the implementation and the interface must match. A method defined as ghost in the interface, must also be implemented as ghost. The same applies to pure methods. An error is reported, for example, when we leave out pure for Inv:

ERROR  *Alpha16Image does not implement the interface Image
	reason: For member Inv, the 'pure' annotation for implementation and interface does not match
(*Alpha16Image) implements Image
^

The remaining methods:

ColorModel is trivially implemented.
For Bounds, we unfold the Mem predicate to obtain the concrete permission to read the field p.Rect.
The method At is the trickiest to verify as we have to prove that the offset in the Pix array is within bounds, which we explain below.


func (p *Alpha16Image) ColorModel() Model { return Alpha16Model }

// @ requires acc(p.Mem(), _)
// @ pure
// @ decreases
func (p *Alpha16Image) Bounds() (r Rectangle) {
	return /*@ unfolding acc(p.Mem(), _) in @*/ p.Rect
}

// @ requires acc(p.Mem(), 1/2)
// @ requires p.Inv()
// @ ensures acc(p.Mem(), 1/2)
// @ ensures p.Inv()
// @ ensures c != nil && c.Valid()
// @ ensures !Point{x, y}.In(p.Bounds()) ==> (c.RGBASpec() == rgba{})
func (p *Alpha16Image) At(x, y int) (c Color) {
	// @ unfold acc(p.Mem(), 1/2)
	if !(Point{x, y}.In(p.Rect)) {
		// @ fold acc(p.Mem(), 1/2)
		return Alpha16{}
	}
	// @ fold acc(p.Mem(), 1/2)
	i := p.PixOffset(x, y)
	// @ unfold acc(p.Mem(), 1/2)
	c = Alpha16{uint16(p.Pix[i+0])*256 + uint16(p.Pix[i+1])}
	// @ fold acc(p.Mem(), 1/2)
	return
}

// PixOffset returns the index of the first element of Pix that corresponds to
// the pixel at (x, y).
// @ requires acc(p.Mem(), 1/4)
// @ requires p.Inv()
// @ requires Point{x, y}.In(p.Bounds())
// @ ensures acc(p.Mem(), 1/4)
// @ ensures p.Inv()
// @ ensures unfolding acc(p.Mem(), 1/4) in 0 <= offset && offset < len(p.Pix)-1
func (p *Alpha16Image) PixOffset(x, y int) (offset int) {
	// @ unfold acc(p.Mem(), 1/4)
	offset = (y-p.Rect.Min.Y)*p.Stride + (x-p.Rect.Min.X)*2
	// @ LemmaMulPos(y-p.Rect.Min.Y, p.Rect.Max.Y-p.Rect.Min.Y-1, p.Stride)
	// @ fold acc(p.Mem(), 1/4)
	return
}

/*@
ghost
requires a <= b
requires c >= 0
ensures a * c <= b * c
decreases
func LemmaMulPos(a, b, c int) {}
@*/

Due to current limitations with bit operations, we replaced the bit-shift (<<) and bitwise OR (|) operations with arithmetic operations. The original source used the following line.

c = Alpha16{uint16(p.Pix[i+0])<<8 | uint16(p.Pix[i+1])}

Note that the rewrite works because p.Pix has elements of type uint8.

We must show that PixOffset returns an offset satisfying 0 <= offset && offset < len(p.Pix) - 1. As Point{x, y} is contained in the rectangle p.Rect, (y-p.Rect.Min.Y) >= 0 and (x-p.Rect.Min.X) >= 0. Since stride is non-negative, 0 <= offset immediately follows.

TODO @João note about non-linear arithmetic

To prove offset < len(p.Pix) - 1, we help Gobra by providing proof annotations. For the sake of explanation, we give verbose annotations. Please note that they are not strictly necessary. In the body of PixOffset above, a reduced proof is given.

We will need the assertions from Inv:

assert 2 * (p.Rect.Max.X - p.Rect.Min.X) == p.Stride && p.Stride * (p.Rect.Max.Y - p.Rect.Min.Y) == len(p.Pix)

First, we define a few ghost variables as abbreviations to simplify the offset calculation. We can assert upper bounds on dx and dy, again since the point is contained in the rectangle.

offset = (y-p.Rect.Min.Y)*p.Stride + (x-p.Rect.Min.X)*2
ghost var height = p.Rect.Max.Y - p.Rect.Min.Y
ghost var dy = y-p.Rect.Min.Y
ghost var dx = (x-p.Rect.Min.X) * 2
assert offset == dy * p.Stride + dx
assert 0 <= dx && 0 <= dy && 0 <= offset
assert dy <= height - 1
assert dx <= p.Stride - 2

Next, we make use of the simple arithmetic fact that for \(a, b, c \in \mathbb{N}\) the following holds: \(a \leq b \implies a \cdot c \leq b \cdot c \). We define this lemma as a ghost function and invoke it with the appropriate arguments.

LemmaMulPos(y-p.Rect.Min.Y, p.Rect.Max.Y-p.Rect.Min.Y-1, p.Stride)

Afterwards, we can rewrite the inequality and arrive at the desired fact.

assert dy * p.Stride + dx <= (height - 1) * p.Stride + dx
assert offset <= (height - 1) * p.Stride + p.Stride - 2
assert offset <= len(p.Pix) - 2

The following example uses *Alpha16Image as an Image:

func clientAlpha() {
	var i Image
	a := &Alpha16Image{
		Pix:    []uint8{0x0, 0x0, 0xff, 0xff, 0xff, 0xff, 0x0, 0x0},
		Stride: 4,
		Rect:   Rectangle{Point{0, 0}, Point{2, 2}},
	}
	// @ fold a.Mem()
	i = a
	i.ColorModel()
	// @ assert i.Inv()
	c := i.At(-1, 0)
	// @ assert(c.RGBASpec() == rgba{})
}

Implementation without memory footprint

A Rectangle is also an Image, with bounds equal to the rectangle itself. For points within the rectangle, Opaque color is returned and Transparent color otherwise. No memory access is required in this case, and no invariant must be preserved. The predicate Mem and the function Inv still have to be defined to implement Image. We simply have true as the body and the return value respectively.

/*@
// Mem implements the [Image] interface.
pred (r Rectangle) Mem() {
	true
}

// Inv implements the [Image] interface.
ghost
decreases
pure func (r Rectangle) Inv() bool {
	return true
}
@*/

// ColorModel implements the [Image] interface.
func (r Rectangle) ColorModel() Model {
	return Alpha16Model
}

// Bounds implements the [Image] interface.
// @ requires acc(r.Mem(), _)
// @ pure
// @ decreases
func (r Rectangle) Bounds() (res Rectangle) {
	return r
}

// At implements the [Image] interface.
// @ preserves acc(r.Mem(), 1/2)
// @ preserves r.Inv()
// @ ensures c != nil && c.Valid()
// @ ensures Point{x, y}.In(r.Bounds()) == (c.RGBASpec() != rgba{})
func (r Rectangle) At(x, y int) (c Color) {
	if (Point{x, y}).In(r) {
		return Alpha16{0xffff} // Opaque
	}
	return Alpha16{0} // Transparent
}

// @ Rectangle implements Image

The full example with all image related interfaces can be found here.

Implementation proofs (`implements`)

In Gobra, a concrete type serving as the underlying type of an interface value must be a behavioral subtype of that interface. An implementation proof is needed when Gobra cannot prove this automatically.

As an example, we consider the interface Bounded with a single method Bounds that returns a bounding rectangle. Additionally, a Mem predicate is defined to abstract memory access.

type Bounded interface {
	// @ pred Mem()

	// @ preserves acc(Mem(), 1/2)
	Bounds() (r Rectangle)
}

type Point struct {
	X, Y int
}

type Rectangle struct {
	Min, Max Point
}

We implement the Bounded interface for the type (*Alpha16Image). With the implementation of Bounds and the predicate Mem, (*Alpha16Image) fulfills all syntactic requirements for the Bounded interface.

type Alpha16Image struct {
	// Pix holds the image's pixels, as alpha values in big-endian format. The pixel at
	// (x, y) starts at Pix[(y-Rect.Min.Y)*Stride + (x-Rect.Min.X)*2].
	Pix []uint8
	// Stride is the Pix stride (in bytes) between vertically adjacent pixels.
	Stride int
	// Rect is the image's bounds.
	Rect Rectangle
}

/*@
pred (p *Alpha16Image) Mem() {
	acc(p) && forall i int :: {&p.Pix[i]} 0 <= i && i < len(p.Pix) ==> acc(&p.Pix[i])
}
@*/

// @ preserves acc(&p.Rect, 1/2)
func (p *Alpha16Image) Bounds() (r Rectangle) {
	return p.Rect
}

The statement T implements I checks whether the type T is a behavioral subtype of the interface type I. Gobra tries an auto-generated proof, which may fail as seen in the following snippet:

// @ (*Alpha16Image) implements Bounded

ERROR Generated implementation proof (*Alpha16Image implements interface{ Bounds }) failed. Precondition of call to implementation method might not hold. 

Permission to p.Rect might not suffice.

The above failed, since obtaining acc(&p.Rect, 1/2) from the interface's precondition acc(Mem(), 1/2) requires folding a predicate instance. Gobra currently does not attempt to show this.

We give an implementation proof following the implements keyword, where we must show that the implementation's precondition holds, given that the interface's precondition holds. After calling the implementation method and establishing its postcondition, we must prove the postcondition of the interface method.

/*@
(*Alpha16Image) implements Bounded {
	(p *Alpha16Image) Bounds() (r Rectangle) {
     	unfold acc(p.Mem(), 1/2)
        r = p.Bounds()
     	fold acc(p.Mem(), 1/2)
        return
    }
}
@*/

For each method, we provide proof annotations in the body. Currently, implementation proofs are subject to strict syntactic restrictions. Besides calling the implementation method, we may only fold predicates and use assert statements. Note that contracts are not repeated in the implementation proof.

In this case, after unfold acc(p.Mem(), 1/2), the precondition of the implementation method holds, and we call p.Bounds(), then assign the out-parameter. After fold acc(p.Mem(), 1/2), the postcondition of the interface method holds. Hence, the implementation proof succeeds.

Predicates in implementation proofs

Predicates defined for an interface must be declared by the implementations. When the implementing type is not the receiver of the predicate or the name of the predicate differs, the correct predicate must be assigned in the implementation proof.

In the above example, we declared the predicate (p *Alpha16Image) Mem(), which required no changes in the implementation proof. Alternatively, consider if we defined the predicate MyMem(p *Alpha16Image). Then we must add the highlighted line to the implementation proof:

/*@
pred MyMem(p *Alpha16Image) {
	acc(p) && forall i int :: {&p.Pix[i]} 0 <= i && i < len(p.Pix) ==> acc(&p.Pix[i])
}
@*/

/*@
(*Alpha16Image) implements Bounded {

	pred Mem := MyMem	// <--- assign the predicate

	(p *Alpha16Image) Bounds() (r Rectangle) {
		unfold acc(MyMem(p), 1/2) // instead of p.Mem()
		r = p.Bounds()
		fold acc(MyMem(p), 1/2)	  // instead of p.Mem()
		return
	}
}
@*/

Implementation proof in different packages

An implementation proof may be placed in a different package from the implementation. Similar to Go, where it is not possible to define new methods on a type from another package, we cannot define a predicate with a receiver from a different package. For example, in the package main, we cannot declare the predicate pred (x *image.Gray) Mem(), so we must resort to something like pred Mem(x *image.Gray). Then the predicate must be assigned in the implementation proof as described above.

An example of this can be found here.

Trivial implementation proofs

Alternatively, we can change the contract of (p *Alpha16Image) Bounds() to match the contract in the interface:

	// @ preserves acc(Mem(), 1/2)
	Bounds() (r Rectangle)

Then we can omit the implementation proof and instead fold and unfold the Mem predicate. In the other sections, most examples use this pattern.

// @ preserves acc(p.Mem(), 1/2)
func (p *Alpha16Image) Bounds() (r Rectangle) {
	// @ unfold acc(p.Mem(), 1/2)
	r = p.Rect
	// @ fold acc(p.Mem(), 1/2)
	return
}

Full example

package bounded

type Bounded interface {
	// @ pred Mem()

	// @ preserves acc(Mem(), 1/2)
	Bounds() (r Rectangle)
}

type Point struct {
	X, Y int
}

type Rectangle struct {
	Min, Max Point
}


type Alpha16Image struct {
	// Pix holds the image's pixels, as alpha values in big-endian format. The pixel at
	// (x, y) starts at Pix[(y-Rect.Min.Y)*Stride + (x-Rect.Min.X)*2].
	Pix []uint8
	// Stride is the Pix stride (in bytes) between vertically adjacent pixels.
	Stride int
	// Rect is the image's bounds.
	Rect Rectangle
}

/*@
pred (p *Alpha16Image) Mem() {
	acc(p) && forall i int :: {&p.Pix[i]} 0 <= i && i < len(p.Pix) ==> acc(&p.Pix[i])
}
@*/

// @ preserves acc(&p.Rect, 1/2)
func (p *Alpha16Image) Bounds() (r Rectangle) {
	return p.Rect
}


/*@
(*Alpha16Image) implements Bounded {
	(p *Alpha16Image) Bounds() (r Rectangle) {
     	unfold acc(p.Mem(), 1/2)
        r = p.Bounds()
     	fold acc(p.Mem(), 1/2)
        return
    }
}
@*/

// @ requires a.Mem()
func client(a *Alpha16Image) {
	var b Bounded = a
	b.Bounds()
}

Case study: `sort.Interface`

In this section, we deepen the concepts introduced in the previous sections on interfaces with a more extensive example from the Go standard library.

The interface Interface is used for various sorting routines in the sort package. This interface describes a collection with a length where elements can be compared and swapped.

As usual, we define a Mem predicate to abstract memory access to the collection. We extend the interface with a View method, abstracting the collection to a sequence so that we can specify the methods in terms of their effect on the abstracted data type.

// https://cs.opensource.google/go/go/+/refs/tags/go1.23.6:src/sort/sort.go;l=118

type Interface interface {
	// @ pred Mem()

	// @ ghost
	// @ requires acc(Mem(), _)
	// @ decreases
	// @ pure View() (ghost seq[any])

	// Len is the number of elements in the collection.
	// @ requires acc(Mem(), 1/1024)
	// @ ensures acc(Mem(), 1/1024)
	// @ ensures res == len(View())
	// @ decreases len(View())
	Len() (res int)

	// Less reports whether the element with index i
	// must sort before the element with index j.
	//
	// If both Less(i, j) and Less(j, i) are false,
	// then the elements at index i and j are considered equal.
	// Sort may place equal elements in any order in the final result,
	// while Stable preserves the original input order of equal elements.
	//
	// Less must describe a transitive ordering:
	// - if both Less(i, j) and Less(j, k) are true, then Less(i, k) must be true as well.
	// - if both Less(i, j) and Less(j, k) are false, then Less(i, k) must be false as well.
	//
	// Note that floating-point comparison (the < operator on float32 or float64 values)
	// is not a transitive ordering when not-a-number (NaN) values are involved.
	// See Float64Slice.Less for a correct implementation for floating-point values.
	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ decreases len(View())
	// @ pure LessSpec(i, j int) bool

	// @ requires acc(Mem(), 1/1024)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ ensures acc(Mem(), 1/1024)
	// @ ensures res == old(LessSpec(i, j))
	// @ decreases len(View())
	Less(i, j int) (res bool)

	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ requires 0 <= k && k < len(View())
	// @ requires LessSpec(i, j) && LessSpec(j, k)
	// @ ensures acc(Mem(), _)
	// @ ensures old(LessSpec(i, k))
	// @ decreases
	// @ LessIsTransitive(i, j, k int)

	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ requires 0 <= k && k < len(View())
	// @ requires !LessSpec(i, j) && !LessSpec(j, k)
	// @ ensures acc(Mem(), _)
	// @ ensures old(!LessSpec(i, k))
	// @ decreases
	// @ LessIsCoTransitive(i, j, k int)

	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ ensures acc(Mem(), _)
	// @ ensures old(!LessSpec(i, i))
	// @ decreases
	// @ LessIsIrreflexive(i int)

	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ requires LessSpec(i, j)
	// @ ensures acc(Mem(), _)
	// @ ensures old(!LessSpec(j, i))
	// @ decreases
	// @ LessIsAsymmetric(i, j int)

	// Swap swaps the elements with indices i and j.
	// @ requires acc(Mem(), 1)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ ensures acc(Mem(), 1)
	// @ ensures let oldView := old(View()) in
	// @ 	let oldi := oldView[i] in
	// @ 	let oldj := oldView[j] in
	// @ 	View() == oldView[i = oldj][j = oldi]
	// @ decreases len(View())
	Swap(i, j int)
}

A pure and ghost analogue, LessSpec, of the Less method is defined so that we can use it in specifications. To couple them together, the result of calling Less is equivalent to the result of calling LessSpec in that state (res == old(LessSpec(i, j))).

Using the abstraction View, we can specify what it means to swap the elements with indices i and j as:

	// Swap swaps the elements with indices i and j.
	// @ requires acc(Mem(), 1)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ ensures acc(Mem(), 1)
	// @ ensures let oldView := old(View()) in
	// @ 	let oldi := oldView[i] in
	// @ 	let oldj := oldView[j] in
	// @ 	View() == oldView[i = oldj][j = oldi]
	// @ decreases len(View())
	Swap(i, j int)

Note we use the sequence update operation to create the sequence oldView[i = oldj][j = oldi] where we exchange two elements. Also, we use the binding let v := e1 in e2 to assign the expression e1 to the variable v in the expression e2.

The ghost methods LessIsTransitive and LessIsCoTransitive formalize the requirements described in the docstring:

	// Less reports whether the element with index i
	// must sort before the element with index j.
	//
	// If both Less(i, j) and Less(j, i) are false,
	// then the elements at index i and j are considered equal.
	// Sort may place equal elements in any order in the final result,
	// while Stable preserves the original input order of equal elements.
	//
	// Less must describe a transitive ordering:
	// - if both Less(i, j) and Less(j, k) are true, then Less(i, k) must be true as well.
	// - if both Less(i, j) and Less(j, k) are false, then Less(i, k) must be false as well.
	//

Furthermore, the ordering described by Less must be irreflexive (no element must be sorted before itself) and asymmetric (if an element a must sort before another element b then the element b must not also sort before a).

To implement the interface, one must implement these ghost methods, or equivalently prove the lemmas that together imply that the relation described by Less is a strict weak ordering.

	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ requires 0 <= k && k < len(View())
	// @ requires LessSpec(i, j) && LessSpec(j, k)
	// @ ensures acc(Mem(), _)
	// @ ensures old(LessSpec(i, k))
	// @ decreases
	// @ LessIsTransitive(i, j, k int)
	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ requires 0 <= k && k < len(View())
	// @ requires !LessSpec(i, j) && !LessSpec(j, k)
	// @ ensures acc(Mem(), _)
	// @ ensures old(!LessSpec(i, k))
	// @ decreases
	// @ LessIsCoTransitive(i, j, k int)
	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ ensures acc(Mem(), _)
	// @ ensures old(!LessSpec(i, i))
	// @ decreases
	// @ LessIsIrreflexive(i int)
	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ requires LessSpec(i, j)
	// @ ensures acc(Mem(), _)
	// @ ensures old(!LessSpec(j, i))
	// @ decreases
	// @ LessIsAsymmetric(i, j int)

Having specified the interface, we can specify and verify other functions from the sort package, such as IsSorted. Previously, we have seen similar functions for concrete types, such as integer arrays or slices. Now we have a function that works for any type implementing Interface.

// IsSorted reports whether data is sorted.
// @ requires data != nil
// @ requires acc(data.Mem(), 1/2)
// @ ensures acc(data.Mem(), 1/2)
// @ ensures res == forall j int :: {data.LessSpec(j, j-1)} 0 < j && j < len(data.View()) ==> !data.LessSpec(j, j-1)
// @ decreases
func IsSorted(data Interface) (res bool) {
	n := data.Len()
	if n <= 1 { // added if s.t. the loop invariant can be established
		return true
	}
	// @ invariant acc(data.Mem(), 1/2)
	// @ invariant 0 <= i && i < len(data.View())
	// @ invariant forall j int :: {data.LessSpec(j, j-1)} i < j && j < len(data.View()) ==> !data.LessSpec(j, j-1)
	// @ decreases i
	for i := n - 1; i > 0; i-- {
		if data.Less(i, i-1) {
			return false
		}
	}
	return true
}

Example implementation: `IntSlice`

As an example, we implement Interface for integer slices.

type IntSlice []int

The Mem predicate wraps access to the slice.

/*@
pred (s IntSlice) Mem() {
	acc(s)
}
@*/

We define Less as s[i] < s[j]. This order is transitive, cotransitive, irreflexive, and asymmetric for integers. No proof annotations are required for this.

// @ ghost
// @ requires acc(s.Mem(), _)
// @ requires 0 <= i && i < len(s.View())
// @ requires 0 <= j && j < len(s.View())
// @ decreases len(s.View())
// @ pure func (s IntSlice) LessSpec(i, j int) (res bool) {
// @ 	return unfolding acc(s.Mem(), _) in s[i] < s[j]
// @ }

// @ requires acc(s.Mem(), 1/1024)
// @ requires 0 <= i && i < len(s.View())
// @ requires 0 <= j && j < len(s.View())
// @ ensures acc(s.Mem(), 1/1024)
// @ ensures res == old(s.LessSpec(i, j))
// @ decreases
func (s IntSlice) Less(i, j int) (res bool) {
	// @ unfold acc(s.Mem(), 1/1024)
	res = s[i] < s[j]
	// @ fold acc(s.Mem(), 1/1024)
	return
}

// @ ghost
// @ requires acc(s.Mem(), _)
// @ requires 0 <= i && i < len(s.View())
// @ requires 0 <= j && j < len(s.View())
// @ requires 0 <= k && k < len(s.View())
// @ requires s.LessSpec(i, j) && s.LessSpec(j, k)
// @ ensures acc(s.Mem(), _)
// @ ensures s.LessSpec(i, k)
// @ decreases
// @ func (s IntSlice) LessIsTransitive(i, j, k int) {}

// @ ghost
// @ requires acc(s.Mem(), _)
// @ requires 0 <= i && i < len(s.View())
// @ requires 0 <= j && j < len(s.View())
// @ requires 0 <= k && k < len(s.View())
// @ requires !s.LessSpec(i, j) && !s.LessSpec(j, k)
// @ ensures acc(s.Mem(), _)
// @ ensures old(!s.LessSpec(i, k))
// @ decreases
// @ func (s IntSlice) LessIsCoTransitive(i, j, k int) {}

// @ ghost
// @ requires acc(s.Mem(), _)
// @ requires 0 <= i && i < len(s.View())
// @ ensures acc(s.Mem(), _)
// @ ensures old(!s.LessSpec(i, i))
// @ decreases
// @ func (s IntSlice) LessIsIrreflexive(i int) {}

// @ ghost
// @ requires acc(s.Mem(), _)
// @ requires 0 <= i && i < len(s.View())
// @ requires 0 <= j && j < len(s.View())
// @ requires s.LessSpec(i, j)
// @ ensures acc(s.Mem(), _)
// @ ensures old(!s.LessSpec(j, i))
// @ decreases
// @ func (s IntSlice) LessIsAsymmetric(i, j int) {}

The abstraction function View converts the slice to a sequence. With the helper function viewAux we recursively construct the sequence while building up the postcondition that we have already converted the current prefix.

// @ ghost
// @ requires acc(s.Mem(), _)
// @ ensures len(res) == len(s)
// @ ensures forall i int :: {res[i]} {s[i]} 0 <= i && i < len(res) ==> unfolding acc(s.Mem(), _) in  res[i] == s[i]
// @ decreases
// @ pure func (s IntSlice) View() (ghost res seq[any]) {
// @ 	return unfolding acc(s.Mem(), _) in s.viewAux(0, seq[any]{})
// @ }

// @ ghost
// @ requires acc(s, _)
// @ requires 0 <= i && i <= len(s)
// @ requires len(prefix) == i
// @ ensures len(res) == len(s)
// @ requires forall i int :: {prefix[i]} {s[i]} 0 <= i && i < len(prefix) ==> prefix[i] == s[i]
// @ ensures forall i int :: {res[i]} 0 <= i && i < len(res) ==> res[i] == s[i]
// @ decreases len(s) - i
// @ pure
// @ func (s IntSlice) viewAux(i int, prefix seq[any]) (ghost res seq[any]) {
// @ 	return i == len(s) ? prefix : s.viewAux(i + 1, prefix ++ seq[any]{s[i]})
// @ }

Len and Swap are implemented straightforwardly as the corresponding operations on the IntSlice. We only have to add fold and unfold statements to convert between the Mem predicate and the permissions to the slice.

// @ requires acc(s.Mem(), 1/1024)
// @ ensures acc(s.Mem(), 1/1024)
// @ ensures res == len(s.View())
// @ decreases
func (s IntSlice) Len() (res int) {
	// @ unfold acc(s.Mem(), 1/1024)
	res = len(s)
	// @ fold acc(s.Mem(), 1/1024)
	return
}

// @ requires acc(s.Mem(), 1)
// @ requires 0 <= i && i < len(s.View())
// @ requires 0 <= j && j < len(s.View())
// @ ensures acc(s.Mem(), 1)
// @ ensures let oldView := old(s.View()) in
// @ 	let oldi := oldView[i] in
// @ 	let oldj := oldView[j] in
// @ 	s.View() == oldView[i = oldj][j = oldi]
// @ decreases
func (s IntSlice) Swap(i, j int) {
	// @ unfold acc(s.Mem(), 1)
	s[i], s[j] = s[j], s[i]
	// @ fold acc(s.Mem(), 1)
}

As the contracts for the implementation methods match the contracts for the interface methods we do not have to give an implementation proof.

// @ IntSlice implements Interface

Having implemented Interface, we may now call IsSorted(x) with IntSlice values:

func client() {
	var x Interface
	var s IntSlice = []int{1, 2, 2}
	// @ fold s.Mem()
	// @ assert len(s) == 3
	x = s
	b := IsSorted(x)
	// @ assert b
	// @ assert len(x.View()) == 3

	// @ assert x.LessSpec(0, 1)
	// @ assert !x.LessSpec(1, 2)
	// @ assert x.LessSpec(0, 2)
	// @ assert x.View()[1] == x.View()[2]
	// @ assert typeOf(x.View()[1]) == type[int]
	if v, ok := x.(IntSlice); ok {
		// @ assert len(v) == 3
	} else {
		// @ assert false
	}
}

Quiz

Full example

package sort

// Copyright 2009 The Go Authors.

// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions are
// met:

//    * Redistributions of source code must retain the above copyright
// notice, this list of conditions and the following disclaimer.
//    * Redistributions in binary form must reproduce the above
// copyright notice, this list of conditions and the following disclaimer
// in the documentation and/or other materials provided with the
// distribution.
//    * Neither the name of Google LLC nor the names of its
// contributors may be used to endorse or promote products derived from
// this software without specific prior written permission.

// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
// OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
// LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

func client() {
	var x Interface
	var s IntSlice = []int{1, 2, 2}
	// @ fold s.Mem()
	// @ assert len(s) == 3
	x = s
	b := IsSorted(x)
	// @ assert b
	// @ assert len(x.View()) == 3

	// @ assert x.LessSpec(0, 1)
	// @ assert !x.LessSpec(1, 2)
	// @ assert x.LessSpec(0, 2)
	// @ assert x.View()[1] == x.View()[2]
	// @ assert typeOf(x.View()[1]) == type[int]
	if v, ok := x.(IntSlice); ok {
		// @ assert len(v) == 3
	} else {
		// @ assert false
	}
}


// IsSorted reports whether data is sorted.
// @ requires data != nil
// @ requires acc(data.Mem(), 1/2)
// @ ensures acc(data.Mem(), 1/2)
// @ ensures res == forall j int :: {data.LessSpec(j, j-1)} 0 < j && j < len(data.View()) ==> !data.LessSpec(j, j-1)
// @ decreases
func IsSorted(data Interface) (res bool) {
	n := data.Len()
	if n <= 1 { // added if s.t. the loop invariant can be established
		return true
	}
	// @ invariant acc(data.Mem(), 1/2)
	// @ invariant 0 <= i && i < len(data.View())
	// @ invariant forall j int :: {data.LessSpec(j, j-1)} i < j && j < len(data.View()) ==> !data.LessSpec(j, j-1)
	// @ decreases i
	for i := n - 1; i > 0; i-- {
		if data.Less(i, i-1) {
			return false
		}
	}
	return true
}

// --------- Interface -----------
// https://cs.opensource.google/go/go/+/refs/tags/go1.23.6:src/sort/sort.go;l=118

type Interface interface {
	// @ pred Mem()

	// @ ghost
	// @ requires acc(Mem(), _)
	// @ decreases
	// @ pure View() (ghost seq[any])

	// Len is the number of elements in the collection.
	// @ requires acc(Mem(), 1/1024)
	// @ ensures acc(Mem(), 1/1024)
	// @ ensures res == len(View())
	// @ decreases len(View())
	Len() (res int)

	// Less reports whether the element with index i
	// must sort before the element with index j.
	//
	// If both Less(i, j) and Less(j, i) are false,
	// then the elements at index i and j are considered equal.
	// Sort may place equal elements in any order in the final result,
	// while Stable preserves the original input order of equal elements.
	//
	// Less must describe a transitive ordering:
	// - if both Less(i, j) and Less(j, k) are true, then Less(i, k) must be true as well.
	// - if both Less(i, j) and Less(j, k) are false, then Less(i, k) must be false as well.
	//
	// Note that floating-point comparison (the < operator on float32 or float64 values)
	// is not a transitive ordering when not-a-number (NaN) values are involved.
	// See Float64Slice.Less for a correct implementation for floating-point values.
	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ decreases len(View())
	// @ pure LessSpec(i, j int) bool

	// @ requires acc(Mem(), 1/1024)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ ensures acc(Mem(), 1/1024)
	// @ ensures res == old(LessSpec(i, j))
	// @ decreases len(View())
	Less(i, j int) (res bool)

	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ requires 0 <= k && k < len(View())
	// @ requires LessSpec(i, j) && LessSpec(j, k)
	// @ ensures acc(Mem(), _)
	// @ ensures old(LessSpec(i, k))
	// @ decreases
	// @ LessIsTransitive(i, j, k int)

	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ requires 0 <= k && k < len(View())
	// @ requires !LessSpec(i, j) && !LessSpec(j, k)
	// @ ensures acc(Mem(), _)
	// @ ensures old(!LessSpec(i, k))
	// @ decreases
	// @ LessIsCoTransitive(i, j, k int)

	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ ensures acc(Mem(), _)
	// @ ensures old(!LessSpec(i, i))
	// @ decreases
	// @ LessIsIrreflexive(i int)

	// @ ghost
	// @ requires acc(Mem(), _)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ requires LessSpec(i, j)
	// @ ensures acc(Mem(), _)
	// @ ensures old(!LessSpec(j, i))
	// @ decreases
	// @ LessIsAsymmetric(i, j int)

	// Swap swaps the elements with indices i and j.
	// @ requires acc(Mem(), 1)
	// @ requires 0 <= i && i < len(View())
	// @ requires 0 <= j && j < len(View())
	// @ ensures acc(Mem(), 1)
	// @ ensures let oldView := old(View()) in
	// @ 	let oldi := oldView[i] in
	// @ 	let oldj := oldView[j] in
	// @ 	View() == oldView[i = oldj][j = oldi]
	// @ decreases len(View())
	Swap(i, j int)
}

// --------- Implementation -----------

type IntSlice []int


/*@
pred (s IntSlice) Mem() {
	acc(s)
}
@*/

// @ ghost
// @ requires acc(s.Mem(), _)
// @ ensures len(res) == len(s)
// @ ensures forall i int :: {res[i]} {s[i]} 0 <= i && i < len(res) ==> unfolding acc(s.Mem(), _) in  res[i] == s[i]
// @ decreases
// @ pure func (s IntSlice) View() (ghost res seq[any]) {
// @ 	return unfolding acc(s.Mem(), _) in s.viewAux(0, seq[any]{})
// @ }

// @ ghost
// @ requires acc(s, _)
// @ requires 0 <= i && i <= len(s)
// @ requires len(prefix) == i
// @ ensures len(res) == len(s)
// @ requires forall i int :: {prefix[i]} {s[i]} 0 <= i && i < len(prefix) ==> prefix[i] == s[i]
// @ ensures forall i int :: {res[i]} 0 <= i && i < len(res) ==> res[i] == s[i]
// @ decreases len(s) - i
// @ pure
// @ func (s IntSlice) viewAux(i int, prefix seq[any]) (ghost res seq[any]) {
// @ 	return i == len(s) ? prefix : s.viewAux(i + 1, prefix ++ seq[any]{s[i]})
// @ }

// @ requires acc(s.Mem(), 1/1024)
// @ ensures acc(s.Mem(), 1/1024)
// @ ensures res == len(s.View())
// @ decreases
func (s IntSlice) Len() (res int) {
	// @ unfold acc(s.Mem(), 1/1024)
	res = len(s)
	// @ fold acc(s.Mem(), 1/1024)
	return
}

// @ ghost
// @ requires acc(s.Mem(), _)
// @ requires 0 <= i && i < len(s.View())
// @ requires 0 <= j && j < len(s.View())
// @ decreases len(s.View())
// @ pure func (s IntSlice) LessSpec(i, j int) (res bool) {
// @ 	return unfolding acc(s.Mem(), _) in s[i] < s[j]
// @ }

// @ requires acc(s.Mem(), 1/1024)
// @ requires 0 <= i && i < len(s.View())
// @ requires 0 <= j && j < len(s.View())
// @ ensures acc(s.Mem(), 1/1024)
// @ ensures res == old(s.LessSpec(i, j))
// @ decreases
func (s IntSlice) Less(i, j int) (res bool) {
	// @ unfold acc(s.Mem(), 1/1024)
	res = s[i] < s[j]
	// @ fold acc(s.Mem(), 1/1024)
	return
}

// @ ghost
// @ requires acc(s.Mem(), _)
// @ requires 0 <= i && i < len(s.View())
// @ requires 0 <= j && j < len(s.View())
// @ requires 0 <= k && k < len(s.View())
// @ requires s.LessSpec(i, j) && s.LessSpec(j, k)
// @ ensures acc(s.Mem(), _)
// @ ensures s.LessSpec(i, k)
// @ decreases
// @ func (s IntSlice) LessIsTransitive(i, j, k int) {}

// @ ghost
// @ requires acc(s.Mem(), _)
// @ requires 0 <= i && i < len(s.View())
// @ requires 0 <= j && j < len(s.View())
// @ requires 0 <= k && k < len(s.View())
// @ requires !s.LessSpec(i, j) && !s.LessSpec(j, k)
// @ ensures acc(s.Mem(), _)
// @ ensures old(!s.LessSpec(i, k))
// @ decreases
// @ func (s IntSlice) LessIsCoTransitive(i, j, k int) {}

// @ ghost
// @ requires acc(s.Mem(), _)
// @ requires 0 <= i && i < len(s.View())
// @ ensures acc(s.Mem(), _)
// @ ensures old(!s.LessSpec(i, i))
// @ decreases
// @ func (s IntSlice) LessIsIrreflexive(i int) {}

// @ ghost
// @ requires acc(s.Mem(), _)
// @ requires 0 <= i && i < len(s.View())
// @ requires 0 <= j && j < len(s.View())
// @ requires s.LessSpec(i, j)
// @ ensures acc(s.Mem(), _)
// @ ensures old(!s.LessSpec(j, i))
// @ decreases
// @ func (s IntSlice) LessIsAsymmetric(i, j int) {}

// @ requires acc(s.Mem(), 1)
// @ requires 0 <= i && i < len(s.View())
// @ requires 0 <= j && j < len(s.View())
// @ ensures acc(s.Mem(), 1)
// @ ensures let oldView := old(s.View()) in
// @ 	let oldi := oldView[i] in
// @ 	let oldj := oldView[j] in
// @ 	s.View() == oldView[i = oldj][j = oldi]
// @ decreases
func (s IntSlice) Swap(i, j int) {
	// @ unfold acc(s.Mem(), 1)
	s[i], s[j] = s[j], s[i]
	// @ fold acc(s.Mem(), 1)
}

// @ IntSlice implements Interface

Interfaces and termination

Termination checking for interfaces is currently buggy.

TODO issue #865
TODO issue #864

If an interface method specifies termination, any implementation method must be proven to terminate. Termination measures must be comparable between the interface and its implementation. For example, if the interface uses a constant termination measure, the implementation must not use a predicate termination measure.

The termination measure of the implementation must be stronger than the termination measure of the interface.

If the constant termination measure is decreases 5, an implementation must use a smaller constant, e.g., decreases 3.

An error is reported if we try to implement sort.Interface, where the implementing Swap method has no termination measure:

ERROR Generated implementation proof (IntSlice implements interface{ View, Len, LessSpec, Less, LessIsConnected, LessIsTransitive, Swap }) failed. Function might not terminate. 

Required termination condition might not hold.

It is admissible for an interface method to not specify termination, but implementation methods may optionally provide termination measures.

If an interface method specifies a termination measure, the implementing method must have a termination measure that is at least as strong.

Comparable interfaces, `isComparable`

Comparing two interfaces may cause a runtime error if both dynamic values are incomparable. For example, slices are not comparable in Go:

func main() {
	var x any = []int{1, 2}
	var y any = []int{3}
	if x == y { // error
	}
}

panic: runtime error: comparing uncomparable type []int

goroutine 1 [running]:
main.main()
	/home/gobra/comparable.go:52 +0x77
exit status 2

Gobra provides the function isComparable, which takes as input an interface value or a type and returns whether it is comparable according to Go. When the value of an implementation is stored in an interface value, Gobra records whether the resulting interface value is comparable. In the following example, we assign the numeric constant 5 to x, which makes it comparable.

func compare(x any) {
	// @ assert !isComparable(type[[]int])
	// @ assert isComparable(type[string])
	x = 5
	// @ assert isComparable(x)
}

As an example, we change the linked List type to store values of type any (which is a shorthand for the empty interface interface{}).

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

Note that we can store arbitrary values in the list, as the empty interface is trivially implemented by every type.

The recursive function Contains that searches the list for a value might panic because of the comparison l.Value == value between possibly incomparable values, which Gobra detects:

// @ requires acc(l.Mem(), 1/2)
// @ pure
// @ decreases l.Mem()
func (l *List) Contains(value interface{}) bool {
	return /*@ unfolding acc(l.Mem(), 1/2) in @*/ l != nil && (l.Value == value || l.next.Contains(value))
}

ERROR Comparison might panic.
 Both operands of l.Value == value might not have comparable values.

To require that the List contains only comparable elements, we define the function Comparable. With isComparable, we state recursively that each element must be comparable.

/*@
ghost
requires acc(l.Mem(), 1/2)
pure
decreases l.Mem()
func (l *List) Comparable() bool {
	return l != nil ==> unfolding acc(l.Mem(), 1/2) in (isComparable(l.Value) && l.next.Comparable())
}
@*/
// @ requires acc(l.Mem(), 1/2)
// @ requires l.Comparable()
// @ pure
// @ decreases l.Mem()
func (l *List) Contains(value interface{}) bool {
	return /*@ unfolding acc(l.Mem(), 1/2) in @*/ l != nil && (l.Value == value || l.next.Contains(value))
}

The following client code verifies.

func client() {
	var l *List = nil
	// @ fold l.Mem()
	l = &List{Value: "hello", next: nil}
	// @ assert isComparable(l.Value)
	// @ fold l.Mem()
	l = &List{Value: 1, next: l}
	// @ fold l.Mem()
	// @ assert l.Contains("hello")
	// @ assert !l.Contains([2]int{0, 1})
}

Comparing two interfaces may cause a runtime error if both dynamic values are incomparable.

The function isComparable takes as input an interface value or a type and returns whether it is comparable according to Go.

Ghost equality `===`, `!==`

The ghost comparison === compares values of arbitrary types by identity and does not panic. If we used the normal equality == instead in the following example, Gobra reports an error since the sequence contains elements of type any which might not be directly comparable.

// @ ghost
// @ decreases
// @ requires 0 <= i && i < len(s)
// @ requires 0 <= j && j < len(s)
// @ requires s[i] == s[j]
// @ func GhostEq(s seq[any], i, j int) {}

ERROR Comparison might panic. 
Both operands of view[i] == view[j] might not have comparable values.

Full example

package main

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


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

/*@
ghost
requires acc(l.Mem(), 1/2)
pure
decreases l.Mem()
func (l *List) Comparable() bool {
	return l != nil ==> unfolding acc(l.Mem(), 1/2) in (isComparable(l.Value) && l.next.Comparable())
}
@*/

// @ requires acc(l.Mem(), 1/2)
// @ requires l.Comparable()
// @ pure
// @ decreases l.Mem()
func (l *List) Contains(value interface{}) bool {
	return /*@ unfolding acc(l.Mem(), 1/2) in @*/ l != nil && (l.Value == value || l.next.Contains(value))
}


func client() {
	var l *List = nil
	// @ fold l.Mem()
	l = &List{Value: "hello", next: nil}
	// @ assert isComparable(l.Value)
	// @ fold l.Mem()
	l = &List{Value: 1, next: l}
	// @ fold l.Mem()
	// @ assert l.Contains("hello")
	// @ assert !l.Contains([2]int{0, 1})
}


func compare(x any) {
	// @ assert !isComparable(type[[]int])
	// @ assert isComparable(type[string])
	x = 5
	// @ assert isComparable(x)
}

Full example: `image`

package image

// Copyright 2009 The Go Authors.

// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions are
// met:

//    * Redistributions of source code must retain the above copyright
// notice, this list of conditions and the following disclaimer.
//    * Redistributions in binary form must reproduce the above
// copyright notice, this list of conditions and the following disclaimer
// in the documentation and/or other materials provided with the
// distribution.
//    * Neither the name of Google LLC nor the names of its
// contributors may be used to endorse or promote products derived from
// this software without specific prior written permission.

// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
// OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
// LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

/*@
ghost type rgba ghost struct {
	r, g, b, a uint32
}

ghost
pure
decreases
func (c rgba) ColorRange() bool {
	return 0 <= c.r && c.r <= c.a && 0 <= c.g && c.g <= c.a &&
		0 <= c.b && c.b <= c.a && c.a <= 0xffff
}
@*/

// Color can convert itself to alpha-premultiplied 16-bits per channel RGBA.
// The conversion may be lossy.
type Color interface {
	// Returns true if the implementation holds a valid color.
	// @ ghost
	// @ pure
	// @ decreases
	// @ Valid() bool

	// @ ghost
	// @ requires Valid()
	// @ ensures c.ColorRange()
	// @ pure
	// @ decreases
	// @ RGBASpec() (ghost c rgba)

	// RGBA returns the alpha-premultiplied red, green, blue and alpha values
	// for the color. Each value ranges within [0, 0xffff], but is represented
	// by a uint32 so that multiplying by a blend factor up to 0xffff will not
	// overflow.
	//
	// An alpha-premultiplied color component c has been scaled by alpha (a),
	// so has valid values 0 <= c <= a.
	// @ preserves Valid()
	// @ ensures RGBASpec() == rgba{r, g, b, a}
	RGBA() (r, g, b, a uint32)
}

// source: https://cs.opensource.google/go/go/+/refs/tags/go1.24.0:src/image/color/color.go;l=10

// Alpha16 represents a 16-bit alpha color.
type Alpha16 struct {
	A uint16
}

/*@
ghost
pure
requires c.Valid()
ensures res.ColorRange()
decreases
func (c Alpha16) RGBASpec() (res rgba) {
	return let a := uint32(c.A) in rgba{a, a, a, a}
}
@*/

/*@
ghost
decreases
pure func (c Alpha16) Valid() bool {
	return 0 <= c.A && c.A <= 0xffff
}
@*/

// @ preserves c.Valid()
// @ ensures c.RGBASpec() == rgba{r, g, b, a}
func (c Alpha16) RGBA() (r, g, b, a uint32) {
	a = uint32(c.A)
	return a, a, a, a
}


// Model can convert any [Color] to one from its own color model. The conversion
// may be lossy.
type Model interface {
	// @ requires c != nil && c.Valid()
	// @ ensures res != nil && res.Valid()
	Convert(c Color) (res Color)
}


// Go stdlib uses the following, which is not legal in Gobra.
// var Alpha16Model Model = ModelFunc(alpha16Model)

type alpha16Model struct{}

var Alpha16Model alpha16Model

// @ requires c != nil && c.Valid()
// @ ensures res != nil && res.Valid()
// @ ensures typeOf(res) == type[Alpha16]
func (_ alpha16Model) Convert(c Color) (res Color) {
	if _, ok := c.(Alpha16); ok {
		return c
	}
	_, _, _, a := c.RGBA()
	return Alpha16{uint16(a)}
}

// @ alpha16Model implements Model

// A Point is an X, Y coordinate pair. The axes increase right and down.
type Point struct {
	X, Y int
}

// In reports whether p is in r.
// @ pure
// @ decreases
func (p Point) In(r Rectangle) (res bool) {
	return r.Min.X <= p.X && p.X < r.Max.X &&
		r.Min.Y <= p.Y && p.Y < r.Max.Y
}

// A Rectangle contains the points with Min.X <= X < Max.X, Min.Y <= Y < Max.Y.
// It is well-formed if Min.X <= Max.X and likewise for Y. Points are always
// well-formed. A rectangle's methods always return well-formed outputs for
// well-formed inputs.
//
// A Rectangle is also an [Image] whose bounds are the rectangle itself. At
// returns color.Opaque for points in the rectangle and color.Transparent
// otherwise.
type Rectangle struct {
	Min, Max Point
}


// Image is a finite rectangular grid of [Color] values taken from a color
// model.
type Image interface {
	// Mem represents the access to the memory of the Image
	// @ pred Mem()	// <----- Predicate member

	// Invariant that holds for valid images
	// @ ghost
	// @ pure
	// @ requires acc(Mem(), _)
	// @ decreases
	// @ Inv() bool

	// ColorModel returns the Image's color model.
	ColorModel() Model

	// Bounds returns the domain for which At can return non-zero color.
	// The bounds do not necessarily contain the point (0, 0).
	// @ requires acc(Mem(), _)
	// @ pure
	// @ decreases
	Bounds() (r Rectangle)

	// At returns the color of the pixel at (x, y).
	// At(Bounds().Min.X, Bounds().Min.Y) returns the upper-left pixel of the grid.
	// At(Bounds().Max.X-1, Bounds().Max.Y-1) returns the lower-right one.
	// @ preserves acc(Mem(), 1/2)
	// @ preserves Inv()
	// @ ensures c != nil && c.Valid()
	// @ ensures !Point{x, y}.In(Bounds()) ==> (c.RGBASpec() == rgba{})
	At(x, y int) (c Color)
}


/*@
// Mem implements the [Image] interface.
pred (r Rectangle) Mem() {
	true
}

// Inv implements the [Image] interface.
ghost
decreases
pure func (r Rectangle) Inv() bool {
	return true
}
@*/

// ColorModel implements the [Image] interface.
func (r Rectangle) ColorModel() Model {
	return Alpha16Model
}

// Bounds implements the [Image] interface.
// @ requires acc(r.Mem(), _)
// @ pure
// @ decreases
func (r Rectangle) Bounds() (res Rectangle) {
	return r
}

// At implements the [Image] interface.
// @ preserves acc(r.Mem(), 1/2)
// @ preserves r.Inv()
// @ ensures c != nil && c.Valid()
// @ ensures Point{x, y}.In(r.Bounds()) == (c.RGBASpec() != rgba{})
func (r Rectangle) At(x, y int) (c Color) {
	if (Point{x, y}).In(r) {
		return Alpha16{0xffff} // Opaque
	}
	return Alpha16{0} // Transparent
}

// @ Rectangle implements Image

var (
	Transparent = Alpha16{0}
	Opaque      = Alpha16{0xffff}
)

// cannot return them in (r Rectangle) At
// Valid might not be asserted for these global variables


// Alpha16Image is an in-memory image whose At method returns [color.Alpha16] values.
type Alpha16Image struct {
	// Pix holds the image's pixels, as alpha values in big-endian format. The pixel at
	// (x, y) starts at Pix[(y-Rect.Min.Y)*Stride + (x-Rect.Min.X)*2].
	Pix []uint8
	// Stride is the Pix stride (in bytes) between vertically adjacent pixels.
	Stride int
	// Rect is the image's bounds.
	Rect Rectangle
}

/*@
pred (p *Alpha16Image) Mem() {
	acc(p) && forall i int :: {&p.Pix[i]} 0 <= i && i < len(p.Pix) ==> acc(&p.Pix[i])
}
@*/


/*@
ghost
requires acc(p.Mem(), _)
pure
decreases
func (p *Alpha16Image) Inv() bool {
	return unfolding acc(p.Mem(), _) in (2*(p.Rect.Max.X-p.Rect.Min.X) == p.Stride &&
    	p.Stride * (p.Rect.Max.Y-p.Rect.Min.Y) == len(p.Pix)) &&
    	forall i int :: {&p.Pix[i]} 0 <= i && i < len(p.Pix) ==> 0 <= p.Pix[i] && p.Pix[i] <= 0xff
}
@*/


func (p *Alpha16Image) ColorModel() Model { return Alpha16Model }

// @ requires acc(p.Mem(), _)
// @ pure
// @ decreases
func (p *Alpha16Image) Bounds() (r Rectangle) {
	return /*@ unfolding acc(p.Mem(), _) in @*/ p.Rect
}

// @ requires acc(p.Mem(), 1/2)
// @ requires p.Inv()
// @ ensures acc(p.Mem(), 1/2)
// @ ensures p.Inv()
// @ ensures c != nil && c.Valid()
// @ ensures !Point{x, y}.In(p.Bounds()) ==> (c.RGBASpec() == rgba{})
func (p *Alpha16Image) At(x, y int) (c Color) {
	// @ unfold acc(p.Mem(), 1/2)
	if !(Point{x, y}.In(p.Rect)) {
		// @ fold acc(p.Mem(), 1/2)
		return Alpha16{}
	}
	// @ fold acc(p.Mem(), 1/2)
	i := p.PixOffset(x, y)
	// @ unfold acc(p.Mem(), 1/2)
	c = Alpha16{uint16(p.Pix[i+0])*256 + uint16(p.Pix[i+1])}
	// @ fold acc(p.Mem(), 1/2)
	return
}

// PixOffset returns the index of the first element of Pix that corresponds to
// the pixel at (x, y).
// @ requires acc(p.Mem(), 1/4)
// @ requires p.Inv()
// @ requires Point{x, y}.In(p.Bounds())
// @ ensures acc(p.Mem(), 1/4)
// @ ensures p.Inv()
// @ ensures unfolding acc(p.Mem(), 1/4) in 0 <= offset && offset < len(p.Pix)-1
func (p *Alpha16Image) PixOffset(x, y int) (offset int) {
	// @ unfold acc(p.Mem(), 1/4)
	offset = (y-p.Rect.Min.Y)*p.Stride + (x-p.Rect.Min.X)*2
	// @ LemmaMulPos(y-p.Rect.Min.Y, p.Rect.Max.Y-p.Rect.Min.Y-1, p.Stride)
	// @ fold acc(p.Mem(), 1/4)
	return
}

/*@
ghost
requires a <= b
requires c >= 0
ensures a * c <= b * c
decreases
func LemmaMulPos(a, b, c int) {}
@*/


func clientAlpha() {
	var i Image
	a := &Alpha16Image{
		Pix:    []uint8{0x0, 0x0, 0xff, 0xff, 0xff, 0xff, 0x0, 0x0},
		Stride: 4,
		Rect:   Rectangle{Point{0, 0}, Point{2, 2}},
	}
	// @ fold a.Mem()
	i = a
	i.ColorModel()
	// @ assert i.Inv()
	c := i.At(-1, 0)
	// @ assert(c.RGBASpec() == rgba{})
}

Only a subset of the Go image package
Combined multiple packages into a single file
- Renamed, e.g., Alpha16Image instead of Alpha16 to not clash with the color Alpha16
Small syntactic changes.
- For example, to insert fold statements before/after return
- Color models not dynamically defined

Goroutines and data races

This section covers goroutines, Go's lightweight threads, and how Gobra excludes data races, i.e., concurrent accesses to the same memory location with at least one modifying access.

As an example, we use the type Counter with a method to Increment its count.

type Counter struct {
	count int
}

// @ requires acc(&c.count)
// @ ensures acc(&c.count)
func (c *Counter) Increment() {
	c.count += 1
}

Goroutines run in the same address space and concurrent calls to Increment cause data races for c.count. For example, running the following snippet a few times, one may observe different values for c.count afterwards.

for i := 0; i < 1000; i++ {
	go ctr.Increment()
}

When a goroutine is dispatched with the go keyword, Gobra checks that the precondition of the function or method holds. After starting the goroutine, we do not know the state of the goroutine; it may be in the middle of execution, or may have already finished. Hence, we do not get to assume the postcondition of the dispatched function or method.

func main() {
	ctr := new(Counter)
	go ctr.Increment()
	go ctr.Increment() // error
}

ERROR Precondition of call might not hold.

go ctr.Increment() might not satisfy the precondition of the callee.

In the above example, the permission acc(&c.count) is not transferred back after the first go ctr.Increment() statement. But to start the second goroutine, acc(&c.count) is required.

With fractional permissions we can split read permissions to multiple goroutines. It is guaranteed that only one thread can have exclusive write permission to a memory location at a time. Concurrent reads do not constitute a data race.

// @ requires acc(&c.count, 1/8)
func (c *Counter) Get() int {
	return c.count
}

// @ requires acc(&ctr.count, 1/2)
func client1(ctr *Counter) {
	go ctr.Get()
	go ctr.Get()
	go ctr.Get()
	go ctr.Get()
}

Go's data race detector

Go comes with a built-in data race detector which can be enabled with the -race flag. Note that only data races are found by dynamically running code. Therefore not all data races are guaranteed to be found by this detector.

On the other hand, Gobra can statically prove the absence of data races in a program by reasoning with permissions.

In our example, a data race is detected.

> $ go run -race counter.go
==================
WARNING: DATA RACE
Read at 0x00c000012168 by goroutine 7:
  main.(*Counter).Increment()
      /home/gobra/counter.go:14 +0x35
  main.main.gowrap2()
      /home/gobra/counter.go:25 +0x17

Previous write at 0x00c000012168 by goroutine 6:
  main.(*Counter).Increment()
      /home/gobra/counter.go:14 +0x47
  main.main.gowrap1()
      /home/gobra/counter.go:24 +0x17

Goroutine 7 (running) created at:
  main.main()
      /home/gobra/counter.go:25 +0x104

Goroutine 6 (finished) created at:
  main.main()
      /home/gobra/counter.go:24 +0x94
==================
Found 1 data race(s)
exit status 66

First-class predicates

Gobra has support for first-class predicates, i.e., expressions with a predicate type. A first-class predicate of type pred(T1, ..., Tn) has arity n with corresponding parameter types T1, ..., Tn.

This section serves as a prerequisite for the next section where we associate a predicate as the invariant of a lock. First-class predicates enables us to use predicates as parameters or return values of functions or methods.

Predicate constructors `P!<...!>`

To instantiate a first-class predicate, Gobra provides predicate constructors. A predicate constructor P!<d1, ..., dn!> partially applies a declared predicate P with the constructor arguments d1, ..., dn. A constructor argument is either a pure expression or a wildcard _, indicating that this argument of P remains unapplied. In particular, the type of P!<d1, ..., dn!> is pred(u1, ..., uk), where u1, ..., uk are the types of the unapplied arguments.

For example, consider the declared predicate Mem:

/*@
pred Mem(x *int8, y *uint32) {
	acc(x) && acc(y)
}
@*/

The predicate constructor Mem!<new(int8), _!> has type pred(*uint32), since the first argument is applied and the second is not. Conversely, Mem!<_, new(uint32)!> has type pred(*int8). Finally, Mem!<new(int8), new(uint32)!> and Mem!< _, _!> have types pred() and pred(*int8, *uint32), respectively.

Note the differences:

Mem(x, y) is an assertion. Short for acc(Mem(x, y), 1), stating that access is held to this predicate instance.
Mem!<x, y!> is a predicate constructor, an expression of type pred().
Mem!<x, y!>() is again an assertion, stating that access is held for this first-class predicate instance.

Equality of first-class predicates

The equality operator for predicate constructors is defined as a point-wise comparison, that is, P1!<d1, ..., dn!> is equal to P2!<d'1, ..., d'n!> if and only if P1 and P2 are the same declared predicate and if di == d'i for all i ranging from 1 to n.

For example, the Mem predicate constructor is equal if all applied arguments are equal. But it is not equal to a different declared predicate such as OtherMem.

// @ requires a == b
func client1(a, b *int8, c *uint32) {
	// @ assert Mem!<a, _!> == Mem!<b, _!>
	// @ assert Mem!<a, c!> == Mem!<b, c!>
	// @ assert OtherMem!<a, c!> == Mem!<a, c!> // error
}

/*@
pred OtherMem(x *int8, y *uint32) {
	acc(x) && acc(y)
}
@*/

ERROR Assert might fail.
Assertion OtherMem!<a, c!> == Mem!<a, c!> might not hold.

`fold` and `unfold` first-class predicates

The body of the predicate P!<d1, ..., dn!> is the body of P with the arguments applied accordingly. Like with other predicates, the first-class predicate P!<d1, ..., dn!> can be instantiated and its instances may occur in assertions and in fold and unfold statements. The fold statement fold P!<d1, ..., dk!>(e1, ..., en) exchanges the first-class predicate instance with its body. The unfold statement does the reverse.

In the following example, we fold and unfold a first-class predicate instance as opposed a normal predicate instance Mem(x, y).

// @ preserves Mem!<x, y!>()
func client2(x *int8, y *uint32) {
	// @ unfold Mem!<x, y!>()
	*x = 1
	*y = 2
	// @ fold Mem!<x, y!>()
}

Reasoning about mutual exclusion with `sync.Mutex`

In this section, we study the Mutex lock from Go's standard library. As an example, we implement and specify SafeCounter, a variation of the Counter from the goroutines example that is safe to use concurrently. We use Mutex to guarantee mutual exclusion, ensuring that at most one goroutine can modify the field count at a time.

import "sync"

// SafeCounter is safe to use concurrently.
type SafeCounter struct {
	mu    sync.Mutex
	count int
}

/*@
pred mutexInvariant(v *int) {
	acc(v)
}

pred (c *SafeCounter) Mem() {
	acc(c.mu.LockP()) && c.mu.LockInv() == mutexInvariant!<&c.count!>
}
@*/

The Mem predicate for *SafeCounter does not directly contain access permissions, but access to the resource c.mu.LockP() that will allow us to Lock the mutex. Additionally, c.mu.LockInv() == mutexInvariant!<&c.count!> specifies the invariant associated with the mutex. LockInv returns a first-class predicate which we compare with the predicate constructor applied with the memory location where count is stored. If we unlock we will get access to an instance of this predicate, allowing us to modify &c.count. To lock, we will have to give up this a predicate instance again.

When we import the sync package, the predefined specs for this package are provided by Gobra. All predefined specs included in Gobra can be found here.

This declares, among others, the methods LockInv, SetInv, and the predicate LockP which are not part of the Go API.

package sync

type Mutex struct {
	state int32
	stema uint32
}

pred (m *Mutex) LockP()
pred (m *Mutex) UnlockP()

ghost
requires inv() && acc(m) && *m == Mutex{}
ensures m.LockP() && m.LockInv() == inv
decreases
func (m *Mutex) SetInv(ghost inv pred())

ghost
requires acc(m.LockP(), _)
decreases _
pure func (m *Mutex) LockInv() pred()

We call them stubs as they are abstract and only the signature with a contract is given. Since no bodies are provided, the contracts are assumed to hold. In the case of Mutex, the specification models the mutual exclusion property.

The ghost method SetInv can be called to initialize a mutex. Access to the mutex (acc(m)) is required and the mutex is zero-valued (*m == Mutex{}, it has not been locked yet). acc(m) is lost, so we may not "tamper" the lock after initialization. To associate the first-class predicate inv with the lock, we need to give up access to an instance inv() of it. Afterwards, LockInv returns the first-class predicate inv and we obtain access to the resource m.LockP().

// @ ensures s.Mem()
func New() (s *SafeCounter) {
	c /*@@@*/ := SafeCounter{}
	// @ fold mutexInvariant!<&c.count!>()
	// @ (c.mu).SetInv(mutexInvariant!<&c.count!>)
	// @ fold c.Mem()
	return &c
}

When constructing a new SafeCounter, we first fold the first-class predicate mutexInvariant<!&c.count!> that denotes the resource protected by the lock. Then, we associate this invariant with the mutex using SetInv. Finally, we can fold the Mem predicate for the SafeCounter.

This way, clients only require holding s.Mem() predicates and we can hide the implementation detail of how access is synchronized with a Mutex, again enforcing the information hiding principle.

Before we annotate the Increment method, consider the specifications of Lock and Unlock:

requires acc(m.LockP(), _)
ensures m.LockP() && m.UnlockP() && m.LockInv()()
func (m *Mutex) Lock()

requires acc(m.LockP(), _) && m.UnlockP() && m.LockInv()()
ensures m.LockP()
decreases
func (m *Mutex) Unlock()

To call either Lock or Unlock, acc(m.LockP(), _) is required. Since the predicate LockP is abstract (it has no body), there is no way for a client to obtain an instance by folding and must have been obtained by SetInv. We may only call Unlock after previously calling Lock. This is modeled by the predicate instance m.UnlockP(), which is required to call Unlock and can only be obtained by calling Lock

// @ requires acc(c.Mem(), _)
func (c *SafeCounter) Increment() {
	// @ unfold acc(c.Mem(), _)
	c.mu.Lock()
	// @ unfold mutexInvariant!<&c.count!>()
	c.count += 1
	// @ fold mutexInvariant!<&c.count!>()
	c.mu.Unlock()
}

From unfolding acc(c.Mem(), _), we obtain acc(m.LockP(), _) and satisfy the precondition of c.mu.Lock. In turn, we get access to the predicate instances m.UnlockP() and m.LockInv()(). Also from c.Mem(), we get that c.mu.LockInv() == mutexInvariant!<&c.count!>. So we can unfold again to get permissions to increment c.count. To Unlock the mutex, the mutexInvariant must be folded back.

As Increment requires only acc(c.Mem(), _), the caller retains acc(c.Mem(), _) and can dispatch the second goroutine. The program verifies.

func main() {
	ctr := New()
	go ctr.Increment()
	go ctr.Increment()
}

Termination in the presence of locks

Programs using locks to synchronize memory access might not terminate. For example, this may happen due to deadlocks, or as in the following snippet, due to forgetting to unlock a mutex. Another thread trying to acquire the lock will block indefinitely. The Lock stub has no decreases clause, so we cannot prove termination of any function, method, or loop that calls this method.

// @ requires acc(c.Mem(), _)
func (c *SafeCounter) Increment() {
	// @ unfold acc(c.Mem(), _)
	c.mu.Lock()
	// @ unfold mutexInvariant!<&c.count!>()
	c.count += 1
	// <----- no Unlock here
}

Gobra also verifies the program with the modified Increment method. It is not enforced that Unlock must be called after Lock. Note that this is sound since mutual exclusion is not violated, and we specify only partial correctness.

Full example

package main

import "sync"

// SafeCounter is safe to use concurrently.
type SafeCounter struct {
	mu    sync.Mutex
	count int
}

/*@
pred mutexInvariant(v *int) {
	acc(v)
}

pred (c *SafeCounter) Mem() {
	acc(c.mu.LockP()) && c.mu.LockInv() == mutexInvariant!<&c.count!>
}
@*/

// @ requires acc(c.Mem(), _)
func (c *SafeCounter) Increment() {
	// @ unfold acc(c.Mem(), _)
	c.mu.Lock()
	// @ unfold mutexInvariant!<&c.count!>()
	c.count += 1
	// @ fold mutexInvariant!<&c.count!>()
	c.mu.Unlock()
}


// @ ensures s.Mem()
func New() (s *SafeCounter) {
	c /*@@@*/ := SafeCounter{}
	// @ fold mutexInvariant!<&c.count!>()
	// @ (c.mu).SetInv(mutexInvariant!<&c.count!>)
	// @ fold c.Mem()
	return &c
}

func main() {
	ctr := New()
	go ctr.Increment()
	go ctr.Increment()
}

Full `sync.Mutex` stubs

// Copyright 2009 The Go Authors. All rights reserved.
// Use of this source code is governed by a BSD-style
// license that can be found in https://golang.org/LICENSE

package sync

type Mutex struct {
	state int32
	stema uint32
}

pred (m *Mutex) LockP()
pred (m *Mutex) UnlockP()

ghost
requires acc(m.LockP(), _)
decreases _
pure func (m *Mutex) LockInv() pred()

ghost
requires inv() && acc(m) && *m == Mutex{}
ensures m.LockP() && m.LockInv() == inv
decreases
func (m *Mutex) SetInv(ghost inv pred())

requires acc(m.LockP(), _)
ensures m.LockP() && m.UnlockP() && m.LockInv()()
func (m *Mutex) Lock()

requires acc(m.LockP(), _) && m.UnlockP() && m.LockInv()()
ensures m.LockP()
decreases
func (m *Mutex) Unlock()

`defer` statements

A defer statement invokes a function whose execution is deferred to the moment the surrounding function returns (spec).

Defer statements are not directly related to concurrency but we include them in this chapter because they frequently occur in concurrent code. For example, a common pattern is to defer the call of the Unlock method for a mutex. Here, we augment the SafeCounter example with a method Get:

// @ requires acc(c.Mem(), 1/4)
// @ ensures acc(c.Mem(), 1/4)
func (c *SafeCounter) Get() int {
	// @ unfold acc(c.Mem(), 1/4)
	// @ defer fold acc(c.Mem(), 1/4) // <-----
	c.mu.Lock()
	defer c.mu.Unlock() // <-----
	// @ unfold mutexInvariant!<&c.count!>()
	// @ defer fold mutexInvariant!<&c.count!>() // <-----
	return c.count
}

func client() {
	ctr := New()
	go ctr.Get()
	go ctr.Get()
	go ctr.Increment()
	go ctr.Increment()
}

We use defer three times, once deferring c.mu.Unlock() and in ghost code to defer folding the predicates mutexInvariant and c.Mem.

At the point defer executes, only the function and parameters are evaluated. Deferred functions or methods are executed in the reverse order they were deferred. Gobra checks the contracts when they are executed.

For example, if we swap the order of the defer statements in the example above, Gobra reports an error since when Unlock is executed, mutexInvariant has not been folded yet.

    // ...
	// @ defer fold mutexInvariant!<&c.count!>()
	defer c.mu.Unlock()
	return c.count

ERROR  Precondition of call might not hold. 
Permission to m.LockInv()() might not suffice.

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.

expression `E`	type of `x`	type of `y`	result type of `E`	description
`x ++ y`	`seq[T]`	`seq[T]`	`seq[T]`	concatenation
`x[i]`	`seq[T]`		`T`	lookup the element at index `i` ¹
`x == y`	`seq[T]`	`seq[T]`	`bool`	equality
`x in y`	`T`	`seq[T]`	`bool`	`true` if and only if `x` is an element of `y`
`seq[T]{}`			`seq[T]`	empty sequence
`seq[T]{x, y}`	`T`	`T`	`seq[T]`	literal²
`seq[x..y]`	`I`	`I`	`seq[I]` ³	integer sequence \( [x, x+1, \ldots, y-1] \)
`len(x)`	`seq[T]`		`int`	length
`x[i = y]`	`seq[T]`	`T`	`seq[T]`	creates a sequence with element `y` at index `i`, otherwise identical to `x`. ¹
`x[i:j]`	`seq[T]`		`seq[T]`	sub-sequence ⁴
`seq(x)`	`seq[T]`		`seq[T]`	conversion from a sequence
`seq(x)`	`seq[T]`		`[N]T`	conversion from an array of length `N`

The indices i and j are of integer type. Requires 0 <= i && i < len(x).

Sequence literals can be constructed with an arbitrary number of elements. The table only contains an example for two elements.

I is an arbitrary integer type (byte, uint8, int, ...)

⁴

Sub-sequence with elements between index i (inclusive) and index j (exclusive). If i < 0 or i is omitted, the lower index is treated as 0. If j > len(x) or j is omitted, the upper index is treated as len(x).

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.

expression `E`	type of `x`	type of `y`	result type of `E`	description
`set[T]{}`			`set[T]`	\( \varnothing \)
`set[T]{x, y}`	`T`	`T`	`set[T]`	\( \{x, y \} \), in general with an arbitrary number of elements.
`x union y`	`set[T]`	`set[T]`	`set[T]`	\( x \cup y \)
`x intersection y`	`set[T]`	`set[T]`	`set[T]`	\( x \cap y \)
`x setminus y`	`set[T]`	`set[T]`	`set[T]`	\( x \setminus y\)
`x subset y`	`set[T]`	`set[T]`	`bool`	\( x \subseteq y\)
`x == y`	`set[T]`	`set[T]`	`bool`	\( x = y\)
`x in y`	`T`	`set[T]`	`bool`	\( x \in y\)
`len(x)`	`set[T]`		`int`	\( \|x\| \)
`x # y`	`T`	`set[T]`	int	1 if \(x \in y\) else 0
`set(x)`	`set[T]`		`set[T]`	conversion from a set
`set(x)`	`seq[T]`		`set[T]`	conversion from a sequence

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.

expression `E`	type of `x`	type of `y`	result type of `E`	description
`mset[T]{}`			`mset[T]`
`mset[T]{x, x}`	`T`	`T`	`mset[T]`	\( \{x, x \} \), in general with an arbitrary number of elements.
`x union y`	`mset[T]`	`mset[T]`	`mset[T]`
`x intersection y`	`mset[T]`	`mset[T]`	`mset[T]`
`x setminus y`	`mset[T]`	`mset[T]`	`mset[T]`
`x subset y`	`mset[T]`	`mset[T]`	`bool`
`x == y`	`mset[T]`	`mset[T]`	`bool`
`x in y`	`T`	`mset[T]`	`bool`
`len(x)`	`mset[T]`		`int`
`x # y`	`T`	`mset[T]`	int	multiplicity of the element `x` in `y`
`mset(x)`	`mset[T]`		`mset[T]`	conversion from a multiset
`mset(x)`	`seq[T]`		`mset[T]`	conversion from a sequence

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.

expression `E`	type of `x`	type of `y`	result type of `E`	description
`dict[K]V{}`			`dict[K]V`	empty dict
`dict[K]V{x: y}`	`K`	`V`	`dict[K]V`	dict literal ⁵
`x == y`	`dict[K]V`	`dict[K]V`	`bool`	equality
`x[y]`	`dict[K]V`	`K`	`V`	lookup the value associated with key `y` ⁶
`m[x = y]`	`K`	`V`	`dict[K]V`	dict with additional mapping `(x, y)`, otherwise identical to the dict `m`
`len(x)`	`dict[K]V`		int	number of keys
`domain(x)`	`dict[K]V`		`set[K]`	set of keys
`range(x)`	`dict[K]V`		`set[V]`	set of values

⁵

In general, more items may be given. For duplicate keys, an error is reported:

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}
    ^

⁶

Requires y in domain(x). Otherwise, an error is reported:

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

Playground

You can edit the code below. Use the buttons to verify it with Gobra or run it as a Go program.

package main

// @ 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
}

Practical Program Verification in Go with Gobra (alpha)