Chapter 1 edits

CONTRIBUTING.md

@@ -39,7 +39,7 @@ Source code can be included in either in markdown code blocks
 ````markdown
 ``` go
 package main
-//@ requires
+// @ requires
 func foo() {
 
 }
@@ -50,7 +50,7 @@ or included
 {{#include examples/dutchflag.gobra}}
 ```
 
-The source files used in this project have the extensions `.go` or `.gobra`. `.go` files consist of compilable Go files with specifications written in comments: `//@ ` signals a single line of specification, whereas comments within delimiters`/*@` and `@*/` signal multi-line specifications.
+The source files used in this project have the extensions `.go` or `.gobra`. `.go` files consist of compilable Go files with specifications written in comments: `// @ ` signals a single line of specification, whereas comments within delimiters`/*@` and `@*/` signal multi-line specifications.
 
 
 ### Code Block Attributes
@@ -93,12 +93,12 @@ type = "MultipleChoice"
 prompt.prompt = """
 **Program 1:**
 ```go
-//@ ensures res >= 0
+// @ ensures res >= 0
 func square(x int) (res int) {
 	return x * x
 }
 r := square(a)
-//@ assert r == a*a
+// @ assert r == a*a
 What is the verification result of **Program 1**?
 """
 prompt.distractors = [

ci/dictionary.txt

@@ -1,4 +1,4 @@
-personal_ws-1.1 en 104 utf-8
+personal_ws-1.1 en 107 utf-8
 Collatz
 Datatypes
 Errorf
@@ -29,6 +29,7 @@ Viper
 Wireguard
 addToSlice
 addToSliceClient
+amongst
 arity
 binarySearch
 bool
@@ -52,6 +53,8 @@ hasNext
 incChannel
 incr
 inlined
+instantiation
+instantiations
 invariants
 isComparable
 isContained

quizzes/basic-ghost-pure.toml

@@ -17,7 +17,7 @@ func fibonacci(n int) (ghost res int) {
 // @ ensures res == fibonacci(n)
 func fibIterative(n int) (res int) {
 	a, b := 0, 1
-	//@ (1)
+	// @ (1)
 	for i := 0; i < n; i++ {
 		a, b = b, a+b
 	}

quizzes/basic-specs.toml

@@ -3,12 +3,12 @@ type = "MultipleChoice"
 prompt.prompt = """
 **Program 1:**
 ```go
-//@ ensures res >= 0
+// @ ensures res >= 0
 func square(x int) (res int) {
 	return x * x
 }
 r := square(a)
-//@ assert r == a*a
+// @ assert r == a*a
 ```
 What is the verification result of **Program 1**?
 """
@@ -25,15 +25,15 @@ type = "MultipleChoice"
 prompt.prompt = """
 **Program 2:**
 ```go
-//@ requires false
+// @ requires false
 func dontCallMe()  {}
 ```
 Which of the following programs containing a function with precondition `false` verify?
 """
 prompt.distractors = [
     """
 ```go
-//@ requires false
+// @ requires false
 func dontCallMe()  {}
 
 func client() {
@@ -44,10 +44,10 @@ func client() {
 ]
 answer.answer = ["""
 ```go
-//@ requires false
+// @ requires false
 func dontCallMe()  {}
 
-//@ requires x % 2 == 1
+// @ requires x % 2 == 1
 func callMeNeither(x int) {
     if x % 2 == 0 {
         dontCallMe()
@@ -57,7 +57,7 @@ func callMeNeither(x int) {
 """,
 """
 ```go
-//@ requires false
+// @ requires false
 func dontCallMe()  {}
 ```
 """

src/SUMMARY.md

@@ -9,14 +9,15 @@
 - [Basic specifications](./basic-specs.md)
   <!-- - [`assert` and `assume`](./assert-assume.md) -->
   <!-- - [requires, ensures, and preserves](./requires-ensures.md)-->
-- [Array Operations](./basic-array.md)
+- [Verifying programs with arrays](./basic-array.md)
 - [Quantifiers (`forall`, `exists`) and Implication (`==>`)](./quantifier.md)
 - [Loops](./loops.md)
-  - [Invariants](./loops-invariant.md)
+  - [Loop Invariants](./loops-invariant.md)
   - [Binary Search](./loops-binarysearch.md)
   - [Range](./loops-range.md)
 - [Overflow Checking](./overflow.md)
 - [Termination](./termination.md)
 - [Ghost Code and Pure Functions](./basic-ghost-pure.md)
 
 # Advanced topics
+- [Quantifier Triggers](./triggers.md)

src/basic-array.md

@@ -1,15 +1,18 @@
-# Array Operations
+# Verifying programs with arrays
 <!--
 explain preconditions of an indexing operation, make it clear that accesses out of bounds are excluded statically -->
 
-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.
+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.
 ``` go
 package main
+
 import "fmt"
+
 func main() {
 	a := [5]int{2, 3, 5, 7, 11}
 	fmt.Println(a[-1]) // invalid index (too small)
@@ -21,11 +24,12 @@ func main() {
 ./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.
-
+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:
 ```go
 package main
+
 import "fmt"
+
 func main() {
 	a := [5]int{2, 3, 5, 7, 11}
 	getItem(a, -1)
@@ -36,26 +40,36 @@ func getItem(a [5]int, i int) {
 	fmt.Println(a[i]) // error
 }
 ```
-If we run the program, we get a _runtime error_:
+Go is memory-safe and checks at _runtime_ whether the index is within bounds:
 ``` sh
 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_.
 ``` go
 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.
+<!-- and postcondition `ensures v == a[i]`. -->
+The indexing operation `a[i]` implicitly has the precondition
+`requires 0 <= i && i < len(a)`.
+By propagating this precondition to the contract of `getItem`, Gobra accepts the function.
+``` go
+// @ requires 0 <= i && i < len(a)
+func getItem(a [5]int, i int) {
+	fmt.Println(a[i])
+}
+```
+Then the calls `getItem(a, -1)` and `getItem(a, 10)` will get rejected.
+<!-- TODO fmt stubs missing (error: got unknown identifier Println)
+There is a punchline missing here. We should show how to fix the verification error for the `getItem` function by adding a precondition and then show that we now have a verification error in the client
+-->
+
+> Gobra statically checks that every access to arrays is within bounds.
 
 <!-- this is also checked in specs (e.g. not well defined) -->