"low" changed to "lowElement", "high" changed to "highElement"

src/01/loops-binarysearch.md

@@ -45,7 +45,7 @@ For the case where `target` is found, `idx` gives its position:
 This contract does not yet capture that `idx` must be the first index where `target` is found or else 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`.
+The elements with an index between `lowElement` and `highElement` 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.
 ``` go does_not_verify
 ~const N = 1000
@@ -54,57 +54,57 @@ We must add several loop invariants until this function satisfies its contract.
 // @ 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)
+	lowElement := 0
+	highElement := len(arr)
 	mid := 0
-	for low < high {
-		mid = (low + high) / 2
+	for lowElement < highElement {
+		mid = (lowElement + highElement) / 2
 		if arr[mid] < target {
-			low = mid + 1
+			lowElement = mid + 1
 		} else {
-			high = mid
+			highElement = mid
 		}
 	}
-	return low, low < len(arr) && arr[low] == target
+	return lowElement, lowElement < len(arr) && arr[lowElement] == target
 }
 ```
 ``` text
 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`.
+The variable `mid` is computed as the average of `lowElement` and `highElement`.
 After comparing `target` with the element `arr[mid]`, we can half the search range:
-If `target` is larger, we search between `mid+1` and `high` in the upper half.
-Otherwise, we search between `low` and `mid` in the lower half.
+If `target` is larger, we search between `mid+1` and `highElement` in the upper half.
+Otherwise, we search between `lowElement` and `mid` in the lower half.
 For this, we need the invariant that `mid` remains a valid index for `arr`:
 ``` go
 	// @ invariant 0 <= mid && mid < len(arr)
 ```
 Let us check whether this invariant works:
 1. Before the first iteration, `mid` is initialized to `0`. Therefore, `0 <= mid && mid < N` trivially holds.
-2. For an arbitrary iteration, assume that the invariant `0 <= mid && mid < N` held before this iteration. Now we must show that after updating `mid = (low + high) / 2`, the invariant still holds (since the rest of the body does not influence `mid`).
-However, this cannot be proven without establishing bounds for `low` and `high`.
+2. For an arbitrary iteration, assume that the invariant `0 <= mid && mid < N` held before this iteration. Now we must show that after updating `mid = (lowElement + highElement) / 2`, the invariant still holds (since the rest of the body does not influence `mid`).
+However, this cannot be proven without establishing bounds for `lowElement` and `highElement`.
 
-We know that `low` and `high` stay between `0` and `len(arr)`,
-and `low` should be smaller than `high`, right?
+We know that `lowElement` and `highElement` stay between `0` and `len(arr)`,
+and `lowElement` should be smaller than `highElement`, right?
 ``` go
-	// @ invariant 0 <= low && low < high && high <= len(arr)
+	// @ invariant 0 <= lowElement && lowElement < highElement && highElement <= len(arr)
 	// @ invariant 0 <= mid && mid < len(arr)
 ```
 ``` text
 ERROR Loop invariant might not be preserved. 
-Assertion low < high might not hold.
+Assertion lowElement < highElement might not hold.
 ```
-The condition `low < high` holds before the first iteration and for every iteration except the last.
+The condition `lowElement < highElement` holds before the first iteration and for every iteration except the last.
 However, an invariant must hold after every iteration, including the last.
-We weaken the condition `low < high` to `low <= high` to address this.
+We weaken the condition `lowElement < highElement` to `lowElement <= highElement` to address this.
 
-Note that after exiting the loop, the loop condition gives `!(low < high)`, while the invariant ensures `low <= high`.
-Together, these imply `low == high`.
+Note that after exiting the loop, the loop condition gives `!(lowElement < highElement)`, while the invariant ensures `lowElement <= highElement`.
+Together, these imply `lowElement == highElement`.
 
 Our next challenge is to find invariants that describe which parts of the array have already been searched and are guaranteed not to contain `target`.
-These invariants, combined with `low == high`, should be sufficient to prove the postcondition by the final iteration.
+These invariants, combined with `lowElement == highElement`, should be sufficient to prove the postcondition by the final iteration.
 Currently, we get the error:
 ``` text
 ERROR Postcondition might not hold. 
@@ -113,30 +113,30 @@ Assertion !found ==> forall i int :: {arr[i]} 0 <= i && i < len(arr) ==> arr[i]
 
 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:]` |
+| `lowElement` | `highElement` | `arr[:lowElement]` | `arr[lowElement:highElement]` | `arr[highElement:]` |
 |-------|--------|-------------|-------------------|----------------|
 | 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`.
+We observe a pattern: the slice `arr[lowElement:highElement]` denotes the part of the array we still have to search for.
+All elements in the prefix `arr[:lowElement]` are smaller than `target`, and all elements in the suffix `arr[highElement:]` are greater than or equal to `target`.
 Translating this into invariants gives:
 ``` go
-	// @ 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]
+	// @ invariant forall i int :: {arr[i]} 0 <= i && i < lowElement ==> arr[i] < target
+	// @ invariant forall j int :: {arr[j]} highElement <= 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 the indices remain within bounds.
+`arr[lowElement-1]` and `arr[highElement]`, while ensuring the indices remain within bounds.
 ``` go
-	// @ invariant low > 0 ==> arr[low-1] < target
-	// @ invariant high < len(arr) ==>  target <= arr[high]
+	// @ invariant lowElement > 0 ==> arr[lowElement-1] < target
+	// @ invariant highElement < len(arr) ==>  target <= arr[highElement]
 ```
 
-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`.
+When exiting the loop, we know that `lowElement == highElement`.
+If `target` is contained in `arr`, it must be located at index `lowElement`, which we check for with `arr[lowElement] == target`.
 By combining all invariants, the postcondition can be proven now.
 However, clients still fail to assert some desired properties.
 
@@ -214,22 +214,22 @@ func FinalClient() {
 // @ 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)
+	lowElement := 0
+	highElement := len(arr)
 	mid := 0
-	// @ invariant 0 <= low && low <= high && high <= len(arr)
+	// @ invariant 0 <= lowElement && lowElement <= highElement && highElement <= 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
+	// @ invariant lowElement > 0 ==> arr[lowElement-1] < target
+	// @ invariant highElement < len(arr) ==> target <= arr[highElement]
+	for lowElement < highElement {
+		mid = (lowElement + highElement) / 2
 		if arr[mid] < target {
-			low = mid + 1
+			lowElement = mid + 1
 		} else {
-			high = mid
+			highElement = mid
 		}
 	}
-	return low, low < len(arr) && arr[low] == target
+	return lowElement, lowElement < len(arr) && arr[lowElement] == target
 }
 ```
 

src/01/overflow.md

@@ -31,40 +31,40 @@ const N = MaxInt64
 // @ 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)
+	lowElement := 0
+	highElement := len(arr)
 	mid := 0
-	// @ invariant 0 <= low && low <= high && high <= len(arr)
+	// @ invariant 0 <= lowElement && lowElement <= highElement && highElement <= 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
+	// @ invariant lowElement > 0 ==> arr[lowElement-1] < target
+	// @ invariant highElement < len(arr) ==> target <= arr[highElement]
+	for lowElement < highElement {
+		mid = (lowElement + highElement) / 2  // <--- problematic expression
 		if arr[mid] < target {
-			low = mid + 1
+			lowElement = mid + 1
 		} else {
-			high = mid
+			highElement = mid
 		}
 	}
-	if low < len(arr) {
-	 	return low, arr[low] == target
+	if lowElement < len(arr) {
+	 	return lowElement, arr[lowElement] == target
 	} else {
-	 	return low, false
+	 	return lowElement, false
 	}
 }
 ```
 ``` text
 ERROR Expression may cause integer overflow.
-Expression (low + high) / 2 might cause integer overflow.
+Expression (lowElement + highElement) / 2 might cause integer overflow.
 ```
-<!-- TODO if it works without error use: `return low, low < len(arr) && arr[low] == target` otherwise explain why not
+<!-- TODO if it works without error use: `return lowElement, lowElement < len(arr) && arr[lowElement] == target` otherwise explain why not
 Relevant issue: https://github.com/viperproject/gobra/issues/816 -->
-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:
+For example, for `lowElement = N/2` and `highElement = N`, the sum `lowElement + highElement` cannot be represented by an `int`, and the result will be negative.
+The solution is to replace the offending statement `mid = (lowElement + highElement) / 2` with:
 ``` go
-mid = (high-low) / 2 + low
+mid = (highElement-lowElement) / 2 + lowElement
 ```
-The subtraction does not overflow since `high >= low` and `low >= 0` holds.
+The subtraction does not overflow since `highElement >= lowElement` and `lowElement >= 0` holds.
 After this change, Gobra reports no errors.
 
 

src/01/termination.md

@@ -164,14 +164,14 @@ Another use case is _gradual verification_ where it can be useful to assume term
 ## Termination of binary search
 Let us look again at the [binary search](./loops-binarysearch.md) example.
 This time, we introduce an implementation error:
-`low` is updated to `low = mid` instead of `low = mid + 1`.
+`lowElement` is updated to `lowElement = mid` instead of `lowElement = mid + 1`.
 `BinarySearchArr` could loop forever, for example, with `BinarySearchArr([7]int{0, 1, 1, 2, 3, 5, 8}, 8)`.
 The function would still verify without `decreases` since only partial correctness is checked.
 <!-- 
 For example for `N=3`, `BinarySearchArr([N]int{1, 2, 3}, 2)` does not terminate.
 	arr := [N]int{1, 2, 3}
 	i := BinarySearchArr(arr, 2)
-low mid high
+lowElement mid highElement
  0 1 3
  1 1 2
     -->
@@ -183,23 +183,23 @@ low mid high
 // @ 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)
+    lowElement := 0
+    highElement := len(arr)
     mid := 0
-    // @ invariant 0 <= low && low <= high && high <= len(arr)
+    // @ invariant 0 <= lowElement && lowElement <= highElement && highElement <= 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
+    // @ invariant lowElement > 0 ==> arr[lowElement-1] < target
+    // @ invariant highElement < len(arr) ==> target <= arr[highElement]
+    // @ decreases highElement - lowElement   // <-- added for termination checking
+    for lowElement < highElement {
+        mid = (lowElement + highElement) / 2
         if arr[mid] < target {
-            low = mid // <--- Implementation Error, should be low=mid+1
+            lowElement = mid // <--- Implementation Error, should be lowElement=mid+1
         } else {
-            high = mid
+            highElement = mid
         }
     }
-    return low, low < len(arr) && arr[low] == target
+    return lowElement, lowElement < len(arr) && arr[lowElement] == target
 }
 
 ```
@@ -208,12 +208,12 @@ 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.
+We might be tempted to try `decreases highElement` or `decreases len(arr)-lowElement` as termination measures for the loop.
 However, this is insufficient since the termination measure must decrease 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`.
+In iterations where we update `lowElement`, `highElement` does not decrease, and vice versa.
+The solution is to combine the two as `decreases highElement - lowElement`.
 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.
+If we change back to `lowElement=mid+1`, the program verifies again.
 
 
 ## Decreases tuple
@@ -222,10 +222,10 @@ Generally, one can specify a list of expressions with `decreases E1, E2, ..., EN
 
 A tuple termination measure decreases based on the [lexicographical order](https://en.wikipedia.org/wiki/Lexicographic_order) of the tuple elements.
 
-For `BinarySearchArr`, we used `decreases high - low`.
+For `BinarySearchArr`, we used `decreases highElement - lowElement`.
 Alternatively, we could use:
 ``` go
-// @ decreases high, len(arr) - low
+// @ decreases highElement, len(arr) - lowElement
 ```
 
 ## TODO Conditional termination with `if` clauses

src/02/slices.md

@@ -245,23 +245,23 @@ func BinarySearch(s []int, target int) (idx int, found bool) {
 	if len(s) == 0 {
 		return 0, false
 	}
-	low := 0
-	high := len(s)
+	lowElement := 0
+	highElement := 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 <= lowElement && lowElement <= highElement && highElement <= 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
+	// @ invariant lowElement > 0 ==> s[lowElement-1] < target
+	// @ invariant highElement < len(s) ==> target <= s[highElement]
+	for lowElement < highElement {
+		mid = (lowElement + highElement) / 2
 		if s[mid] < target {
-			low = mid + 1
+			lowElement = mid + 1
 		} else {
-			high = mid
+			highElement = mid
 		}
 	}
-	return low, low < len(s) && s[low] == target
+	return lowElement, lowElement < len(s) && s[lowElement] == target
 }
 
 func client() {