Overview

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

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

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

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

Basic Specifications

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

For example, we give a contract for the function Abs that computes the absolute value of a x int32. Mathematically speaking, Abs(x) should return \( |x| \). 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. We could test the expected result for some cases like Abs(-5) == 5, Abs(0) == 0, and Abs(1) == 1, but is this enough?

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

There is a subtle bug, which Gobra detects with overflow checking enabled:

ERROR Expression -x might cause integer overflow.

By two's complement arithmetic there is one more negative integer and negating the smallest int32 causes overflow: Abs(-2147483648) returns -2147483648 which would clearly violate the postcondition that the result is non-negative. We complete the contract for Abs with a precondition, such that we cannot call Abs for this value:

const MinInt32 = -2147483648  // -1<<32
//@ requires x != MinInt32
//@ ensures res >= 0 && (res == x || res == -x)
func Abs(x int32) (res int32)

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

It is the programmer's job to write the specification, as well as any proof annotations, and it is Gobra's job to check that the proof that a function satisfies its contract is correct. These checks happen statically. 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.

Preconditions with requires

Preconditions are added with the keyword requires before a function declaration. In Go programs, we write Gobra annotations in special line comments starting with //@.

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.

Let us exemplify this with the absolute value example:

package abs

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)

assert

Gobra can be instructed to perform checks with the assert statement.

Gobra checks that the assertion holds and reports an error if it cannot prove it.

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.

Postconditions with ensures

Postconditions are added with the keyword ensures before a function declaration. By convention, they are written after any preconditions.

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

In the absolute value example, we have already seen the precondition res >= 0 && (res == x || res == -x). Assertions are included in the program to show the information Gobra has at the respective program locations. At the beginning of the function, the precondition holds. Depending on the branch taken, different constraints hold for x. In this example, the postcondition must be proven to hold at both return locations. After the calls to Abs, the caller can assert the postcondition.

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
}

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

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

Default Precondition and Postcondition

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

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

func foo() int

is equivalent to

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

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

Quiz

Array Operations

In this section, we operate with arrays of fixed size N. Note that an array is a value and therefore copied when passed to a function. Later we will also look at slices.

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

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

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

But when we wrap the access in a function, Go no longer statically detects the out-of-bounds index.

package main
import "fmt"
func main() {
	a := [5]int{2, 3, 5, 7, 11}
	getItem(a, -1)
	getItem(a, 1)
	getItem(a, 10)
}
func getItem(a [5]int, i int) {
	fmt.Println(a[i]) // error
}

If we run the program, we get a runtime error:

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

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

Note that Go is memory-safe and checks if the index is in range. 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 v := a[i] implicitly has the precondition requires 0 <= i && i < len(a) and postcondition ensures v == a[i] Unfortunately, we can not chain the comparisons and 0 <= i < len(a) is not a valid Gobra assertion.

Quantifiers and Implication

Let us try to write an assertion that states that an array is sorted. We can later use this as a precondition for a binary search function. As a first attempt we might write requires arr[0] <= arr[1] <= arr[2] <= ... <= arr[N-1] Of course, we do not want to write specifications like this since this does not scale and would not work for different lengths N.

Another way of specifying that an array is sorted is that for any two elements of the array, the first element must be less than or equal to the second element.

Universal quantifier forall

In Gobra, for any is realized by the forall quantifier. We cannot directly pick any two elements, but we can state that for any indices i and j of type int, arr[i] <= arr[j] as requires forall i, j int :: arr[i] <= arr[j] Note that we can quantify i and j at the same time, instead of the more cumbersome requires forall i int :: forall j int :: arr[i] <= arr[j]

Array indices must also be in bounds for specifications. We need to constrain that i and j are valid indices, otherwise, we see errors like:

Method contract is not well-formed. 
Index i into arr[i] might be negative.

Implication ==>

In Gobra the operator for the implication¹ if P then Q is ==>. This gives our final version for the precondition:

requires forall i, j int :: 0 <= i && i < j && j < len(arr) ==> arr[i] <= arr[j]
func search(arr [N]int)

Existential Quantifier exists

The existential quantifier exists uses the same syntax (exists IDENTIFIER [,IDENTIFIER]* T :: ASSERTION). As the name suggests, exists requires the assertion to be true for at least one value.

For example, we could state arr contains the value 0 as

exists i int :: 0 <= i && i < len(arr) ==> arr[i] == 0

exists should be used sparingly. It can be a heavy burden for the verifier to find a witness among many possible values. We show later how we could use a ghost return value instead.

Footnotes

Loops

Reasoning with loops introduces a challenge for verification. Loops could execute an unbounded number of iterations. Similar to pre and postconditions for functions, we have to write a specification for a loop in the form of an invariant.

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 over a range.

Termination of loops will be discussed in the next section.

Invariants

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

The loop invariant is valid if it holds...

1. before the first iteration after performing the initialization statement
2. after every iteration
3. when exiting the loop

In Gobra we can specify it with the invariant keyword before a loop.

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

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

Binary Search

We will follow along the example of function binarySearch(arr [N]int, value int) (idx int) that efficiently finds the rightmost position idx in a sorted array of integers arr where value would be inserted according to the sorted order. Our approach is to gradually add specifications and fix errors along the way. If you want to see the final code only you can skip to the end of this chapter.

Let us begin by writing the specification. First, we must require the arr to be sorted. We have already seen how we can write this as a precondition:

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

To understand the the behavior we want to achieve we can look at a small example. Note that for values like 1 contained in arr we want the index just after the last occurrence of that value to be returned.

arr := [7]int{0, 1, 1, 2, 3, 5, 8}
binarySearch(arr, -1) == 0
binarySearch(arr, 0) == 1
binarySearch(arr, 1) == 3
binarySearch(arr, 8) == 7
binarySearch(arr, 9) == 7

All values to the left of idx should compare less or equal to value and all values from idx to the end of the array should be strictly greater than value.

ensures forall i int :: 0 <= i && i < idx ==> arr[i] <= value
ensures forall j int :: idx <= j && j < len(arr) ==> value < arr[j]

Something is still missing. An issue is that the Index j into arr[j] might be negative since we only have idx <= j and no lower bound for idx. Similarly, the Index i into arr[i] might exceed sequence length. After constraining idx to be between 0 and N we are ready to implement binarySearch:

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

We will have to add several invariants until we can verify the function.

First Gobra complains that the Index mid into arr[mid] might be negative.

So our first invariant is, that mid remains a valid index for arr:

	// @ invariant 0 <= mid && mid < N

Let's check manually if this invariant works.

1. Before the first iteration mid is initialized to N / 2 hence 0 <= N / 2 && N / 2 < N trivially holds.
2. For an arbitrary iteration, we assume that before this iteration 0 <= mid && mid < N was true. Now we need to show that after updating mid = (low + high) / 2 the invariant is still true (the rest of the body does not influence mid). But we fail to do so as the invariant does not capture the values low and high.

So let us add what we know about low and high to help the verifier.

	// @ invariant 0 <= low && low < high && high < N
	// @ invariant 0 <= mid && mid < N

With this change we fixed the Index-Error but are confronted with a new error.

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

While low < high is true before the first iteration (assuming N>0) and holds by the loop condition at the beginning of every except the last iteration. But an invariant must hold after every iteration, including the last. This is achieved by changing low < high to low <= high.

Note that after exiting the loop we know !(low < high) because the loop condition must have failed and low <= high from the invariant. Together this implies low == high.

Our next challenge is:

Postcondition might not hold. 
Assertion forall i int :: 0 <= i && i < idx ==> arr[i] <= value might not hold.

So we need to find assertions that describe which parts of the array we have already searched. The goal is that after the last iteration the invariants together with low == high should be able prove the postconditions.

For this step it is useful to think about how binary search works. The slice arr[low:high] denotes the part of the array we still have to search for and which is halved every iteration. In the prefix arr[:low] are no elements larger than value and in the suffix arr[high:] no elements smaller or equal than value. Exemplified for binarySearch([7]int{0, 1, 1, 2, 3, 5, 8}, 4):

Translating the above into Gobra invariants gives:

// @ invariant forall i int :: 0 <= i && i < low ==> arr[i] <= value
// @ invariant forall j int :: high <= j && j < N ==> value < arr[j]

When the function returns, idx == low holds and as discussed above also low == high. We can clearly see that low and high with idx yields the postconditions:

// @ ensures forall i int :: 0 <= i && i < idx ==> arr[i] <= value
// @ ensures forall j int :: idx <= j && j < len(arr) ==> value < arr[j]

Now we can be happy because Gobra found no errors.

We will see binarySearch search again when we look at termination and do overflow checking.

Full Example

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

Range Loops

Go supports loops iterating over a range clause. In this section we use arrays, later we will also iterate over slices and maps. Gobra does not support ranges over integers, strings, slices, and functions.

We are given code that verifies containing the following loop iterating over an integer array:

// @ requires len(arr) > 0
// @ ensures forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> res >= arr[i]
func almostMax(arr [N]int) (res int) {
    //@ invariant 0 <= i && i <= len(arr)
    //@ invariant forall k int :: {arr[k]} 0 <= k && k < i ==> res >= arr[k]
    for i := 0; i < len(arr); i += 1 {
        if arr[i] > res {
            res = arr[i]
        }
    }
    return
}

But if we refactor it using a range clause we face an error:

// @ requires len(arr) > 0
// @ ensures forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> res >= arr[i]
func almostMax(arr [N]int) (res int) {
    //@ invariant 0 <= i && i <= len(arr)
    //@ invariant forall k int :: {arr[k]} 0 <= k && k < i ==> res >= arr[k]
    for i, a := range arr {
        if a > res {
            res = a
        }
    }
    return
}

Postcondition might not hold. 
Assertion forall i int :: 0 <= i && i < len(arr) ==> res >= arr[i] might not hold.

For loops, the general pattern is that the negation of the loop condition together with the invariant imply the postcondition. In the standard for loop, we can deduce that i == len(arr) after the last iteration while it is len(arr)-1 in the range version.

We can specify an additional loop variable defined using with i0 after range. The invariant 0 <= i0 && i0 <= len(arr) holds as well as i0 < len(arr) ==> i == i0. Additionally, i0 will be equal to len(arr) at the end of the loop. Hence if we replace i with i0 in the second invariant, Gobra can infer the postcondition. We no longer need the invariant constraining i and our final verifying version is:

package main
const N = 42
// @ requires len(arr) > 0
// @ ensures forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> res >= arr[i]
func almostMax(arr [N]int) (res int) {
	res = arr[0]
	//@ invariant forall k int :: {arr[k]} 0 <= k && k < i0 ==> res >= arr[k]
	for _, a := range arr /*@ with i0 @*/ {
		if a > res {
			res = a
		}
	}
    return
}

Overflow Checking

Usage

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 64 bit integers. This can be overridden with the --int32 flag.

Binary Search Example

If we check our binary search program with overflow checking enabled, Gobra reports that

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

For example if low = 2 and high = MaxInt64 - 1 their sum cannot be represented by an int64 and the result will be negative.

The solution is to replace the offending statement with mid = (high-low)/2 + low.

After this change, Gobra reports no errors.

If we tweak the const N that denotes the array length to 2147483648 which is larger than MaxInt32 we get an error if we check with the --int32 flag but otherwise verification succeeds.

This bug was actually in Java's standard library (Read All About It: Nearly All Binary Searches and Mergesorts are Broken). We think this highlights why heavily used code should be verified.

Termination

Having talked about loops, the next thing to address is termination. Here we look at the termination of loops and recursive functions. In general, this problem is a hard problem¹. However, for functions we write in practice, it is usually not hard to show termination. Informally it is often clear to argue for (non-)termination. Sometimes, we might even desire non-termination for some functions, e.g. a web server that continuously serves requests.

Partial and Total Correctness

By default, Gobra does not check for termination and proves only partial correctness. For functions, this means that if a function terminates its postcondition can be asserted. Total correctness additionally requires termination.

For example, the following program verifies even though infiniteZero contains an infinite loop.

ensures res == 0
func infiniteZero() (res int) {
    for {}
    return 0
}
func client() {
    r := infiniteZero()
    assert r == 0
}

This behavior is intended since the verifier checks that

1. assuming that infiniteZero terminates then the postcondition res == 0 holds.
2. While never reached in practice, the assertion r == 0 should also hold since the client can deduce this from the postcondition.

Termination Measures and 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 after the invariants. Sometimes, this suffices and a termination measure can be automatically inferred. For example, for simple functions like:

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 is an expression that 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.

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

	//@ decreases len(arr) - i
	for i:=0; i<N; i++ {
		if arr[i] > res {
			res = arr[i]
			idx = i
		}
	}

Binary Search Termination

Let us look again at the binary search example. We might forget to add one and update low = mid instead of low = mid + 1.

    mid = (high-low)/2 + low
    if arr[mid] <= value {
        low = mid
    } else {
        high = mid
    }

For example for N=3, binarySearch([N]int{1, 2, 3}, 2) does not terminate. But the program still verifies since only partial correctness is checked.

This changes when we add decreases.

// @ decreases
func binarySearch(arr [N]int, value int) (idx int) {

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

If we fix the error and change the update back to low = mid + 1 we still get the same error. That is due to the loop for which we have to specify a termination measure as well. We might be tempted to try decreases high or decreases N-low as termination measures. 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. It can be helpful to think of the interpretation for the algorithm. In this case high - low denotes the length of the subarray that we have not checked yet. Now the program verifies again.

Wildcard Termination Measure _

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

The wildcard termination measure _ should be used carefully, especially in conjunction with pure functions. Contradictions can arise if we specify that a function terminates that does not terminate.

decreases _
ensures false
pure
func infiniteRecursion() {
	infiniteRecursion()
	assert 0 != 1
}

Because of the wildcard measure the verifier assumes that infiniteRecursion terminates. Then assertion verifies since the postcondition of infiniteRecursion establishes false from which we can prove any assertion, including logical inconsistencies like 0 != 1.

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.

Full Syntax

"decreases" [expressionList] ["if" expression]

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 over the tuple elements.

For binarySearch we used decreases high - low. Alternatively, we could use decreases high, N - low

Conditional

When we want to prove termination only under certain conditions we can add an if clause at the end.

One is allowed to add only a single clause per kind of termination measure (tuple or wildcard). But we can have a clause for a tuple termination measure while using the wildcard termination measure in other cases. But when the condition held for a tuple measure, this same measure must decrease for all further recursive invocations and can not downgrade to a wildcard measure.

Mutual Recursion

Gobra can also handle termination for mutual recursive functions. For them, the termination measure must decrease for each indirect call.

Quiz

Summary

• By default, Gobra checks for partial correctness.
• For a naked decreases, Gobra attempts to prove termination automatically.
• decreases _ assumes termination, _ is called the wildcard termination measure.

In the next section, we discuss why pure and ghost functions must have termination measures.

Background

If you could find a termination measure for the function Collatz you would solve a famous mathematical problem.

//@ requires n >= 1
func Collatz(n int) int {
    if n == 1 {
        return 1
    } else if n % 2 == 0 {
        return Collatz(n / 2)
    } else {
        return Collatz(3 * n + 1)
    }
}

Ghost Code and pure Functions

Often, introducing additional state, such as additional variables or arguments is useful for specification and verification.

We call code ghost that exists solely for the purpose of verification. It vanishes when the program is compiled. Hence non-ghost code is not allowed to refer to any ghost code. When writing Gobra annotations in Go source files, the syntax //@ makes it clear that the line is treated as a comment by Go and not included in the program.

A function that is deterministic and has no side effects can be marked as pure and may be used in specifications. This allows us to abstract specifications.

A pure and ghost Function

In the binary search section, we relied on the precondition that an array arr is sorted:

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

If we want to write clients that use binarySearch we have to propagate the preconditions, for example, we might want to write insert:

// @ requires forall i, j int :: 0 <= i && i < j && j < len(arr) ==> arr[i] <= arr[j]
func insert(arr [N]int, value int) {
	var fresh [N + 1]int
	idx := binarySearch(arr, value)
    // ...
}

In the spirit of don't repeat yourself we want to abstract the precondition. Our first attempt is:

func isArraySorted(arr [N]int) bool {
	//@ invariant 1<=i && i <= len(arr)
	for i:=1; i<len(arr); i++ {
		if arr[i-1] > arr[i] {
			return false
		}
	}
	return true
}

//@ requires isArraySorted(arr)
func insert(arr [N]int, value int) {
    // ...
}

But we get the error:

error: ghost error: Found call to non-ghost impure function in ghost code
requires isArraySorted(arr)
         ^

Recall:

Assertions are boolean expressions that are deterministic and have no side effects.

We are not allowed to call arbitrary functions in specifications! Here are two simple functions with a side effect or with nondeterminism:

import "time"
var x = 0
func sideEffect(p *int) int {
    *p += 1
    return 0
}
func nonDeterministic() int {
    return int(time.Now().UnixNano() % 100)
}

Actually isArraySorted has no side effects. But Gobra does not automatically infer this. This is where pure comes into play.

We can mark a function with the pure keyword. Note that it must come before func and after the pre and postconditions.

//@ pure
func isArraySorted(arr [N]int) bool {
	//@ invariant 1<=i && i <= len(arr)
	for i:=1; i<len(arr); i++ {
		if arr[i-1] > arr[i] {
			return false
		}
	}
	return true
}

error: For now, the body of a pure block is expected to be a single return with a pure expression, got Vector(  omitted...

Due to the syntactical restrictions, we need another way to express it. As an attempt, we could try to return the assertion from the precondition:

func isSorted(arr [N]int) bool {
	return forall i, j int :: 0 <= i && i < j && j < len(arr) ==> arr[i] <= arr[j]
}

But forall is not valid in Go code. We can make the function ghost by inserting the ghost keyword before the other specifications:

/*@ 
ghost
pure
decreases
func isSorted(arr [N]int) bool {
	return forall i, j int :: 0 <= i && i < j && j < len(arr) ==> arr[i] <= arr[j]
}
@*/

//@ requires isSorted(arr)
func insert(arr [N]int, value int) {
    // ...
}

The above version verifies. Note that we had to add decreases; we explain shortly why this is necessary.

Fibonacci

While recursion is not idiomatic in Go it is often used for specifications. As an example, we look at the famous fibonacci function. Due to the syntactical limitations of pure functions, we are not allowed to use if statements in their bodies. Instead, we resort to the conditional expression cond ? e1 : e2:

// @ 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) {
                       ^

We got an error because Go does not support the ternary operator and fibonacci's body contains ghost code. The error can be avoided by declaring the out parameter as (ghost res int) but it is preferred to make the entire function ghost:

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

Note that we do not have to specify postconditions. As opposed to normal functions where we cannot peek inside them, calls to pure functions can be thought of as inlined. The following assertions pass:

/*@
ghost
decreases
func client(n int) {
	if n > 1 {
		assert fibonacci(n) == fibonacci(n-1) + fibonacci(n-2)
    }
    if n == 0 {
    	assert fibonacci(0) == 0
    }
}@*/

We leave it as an exercise in the Quiz to provide invariants for an iterative implementation satisfying the specification:

// @ requires n >= 0
// @ ensures res == fibonacci(n)
func fibIterative(n int) (res int)

Ghost Erasure

Ghost code must not affect actual code. The behavior of a program with ghost code, and with ghost code erased must be the same. For example, if we try to modify a variable x with a ghost statement. To make a statement ghost, add ghost before it.

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

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

Gobra detects that modifying x could clearly alter the output of the program.

The control flow must also not diverge. We are not allowed to make any statement ghost, for example if we try to exit early out of the function loop, this would change its (termination) behavior.

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

But this is not permitted:

ghost error: expected ghostifiable statement

Termination of ghost functions

Termination measures must be provided for ghost functions. This is also to ensure that their presence does not change the program's behavior. As a simple example, assume that inf() does not terminate.

func boo()  {
	//@ ghost y := inf()
	return 0
}

Clearly, boo loops with ghost code and returns immediately without.

Termination of pure functions

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

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 _ // assume termination
ensures res != 0
func incons(x int) (res int) {
	return 2 * incons(x)
}

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

The assertions all pass since

1. We saw that we can replace the call of a pure function with its body.
2. Divide both sides by incons(1) (what would happen without the precondition ensures res != 0? ¹)
3. Arithmetic
4. We found the contradiction 1 == 2, or equivalently false.

Ghost Parameter

Let us look at the function max that returns the maximum element of a non-empty array with signature:

//@ requires len(arr) > 0
//@ 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 [N]int) (res int)

Verifying this function would be challenging because of the exists 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.

//@ requires len(arr) > 0
//@ 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]
    //@ idx = 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
			//@ idx = i
		}
	}
	return res /*@ , idx @*/
}

Now when calling max we must also assign to a ghost variable:

arr := [N]int{-2, 2, 1, 5, 5}
//@ ghost var idx int
m, /*@ idx @*/ := max(arr)

More Ghosts

In general, in Gobra there are:

• ghost in and out parameters ghost idx, int
• ghost functions where all in- and out-parameters are implicitly ghost
• ghost methods
• ghost variables ghost var x int = 42
• ghost statements (if-then-else, loops)
• ghost types (e.g. sequences, sets, multisets)

We will continue to use ghost code in the following chapters.

Quiz

Footnotes

Assert might fail. 
Divisor incons(1) might be zero.