Skip to content

Commit

Permalink
chore: tabs instead spaces
Browse files Browse the repository at this point in the history
  • Loading branch information
@gottschali
gottschali committed Jan 29, 2025
1 parent 519cf9b commit df91faa
Show file tree
Hide file tree
Showing 3 changed files with 83 additions and 83 deletions.
48 changes: 24 additions & 24 deletions src/ghost.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,17 +31,17 @@ 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 @*/
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() {
Expand All @@ -63,27 +63,27 @@ 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:
``` go
var x int
// @ ghost x = 1
// ...
var x int
// @ ghost x = 1
// ...
```
``` text
ERROR ghost error: only ghost locations can be assigned to in ghost code
```
<!-- TODO Limitation: if the statement is not made ghost, there is no error but it updates the variable!
var x int
// @ x = 1
// @ assert x == 1
// @ assert x == 0 // ERROR
var x int
// @ x = 1
// @ assert x == 1
// @ assert x == 0 // ERROR
-->

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:
``` go
func loop() {
// @ ghost return
for {}
// @ ghost return
for {}
}
```
``` text
Expand All @@ -99,19 +99,19 @@ For example, the function `boo` does not terminate with ghost code but returns i
/*@
ghost
func inf() {
for {}
for {}
}
@*/

// @ decreases
func boo() int {
// @ ghost inf()
return 42
// @ ghost inf()
return 42
}
```
``` text
ERROR loop occurring in ghost context does not have a termination measure
for {}
for {}
^
```

Expand Down
52 changes: 26 additions & 26 deletions src/pure.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,19 +8,19 @@ If we try to call a normal Go function `Cube` in an assert statement, Gobra repo
package main

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

func client() {
// @ assert 8 == Cube(2)
// @ assert 8 == Cube(2)
}
```
``` text
ERROR /tmp/playground.go:8:9:error: expected pure expression, but got '8 == Cube(3)'
assert 8 == Cube(3)
assert 8 == Cube(3)
^
ERROR /tmp/playground.go:8:14:error: ghost error: Found call to non-ghost impure function in ghost code
assert 8 == Cube(3)
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.
Expand All @@ -29,15 +29,15 @@ Gobra enforces the syntactic requirement that the body of `pure` functions must
// @ pure
// @ decreases
func Cube(x int) int {
return x * x * x
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
// @ 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.
Expand Down Expand Up @@ -124,11 +124,11 @@ Hence, we are unable to define `fibonacci` with an `if` statement:
// @ pure
// @ decreases n
func fibonacci(n int) (res int) {
if n <= 1 {
return n
} else {
return fibonacci(n-1) + fibonacci(n-2)
}
if n <= 1 {
return n
} else {
return fibonacci(n-1) + fibonacci(n-2)
}
}
```
``` text
Expand Down Expand Up @@ -189,8 +189,8 @@ 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`.
``` go
func client2() {
// @ assert fibonacci(3) == fibonacci(2) + fibonacci(1)
// @ assert fibonacci(3) == 2
// @ assert fibonacci(3) == fibonacci(2) + fibonacci(1)
// @ assert fibonacci(3) == 2
}
```
``` text
Expand All @@ -201,10 +201,10 @@ 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)`.
``` go
func client3() {
// @ assert fibonacci(0) == 0
// @ assert fibonacci(1) == 1
// @ assert fibonacci(2) == 1
// @ assert fibonacci(3) == 2
// @ assert fibonacci(0) == 0
// @ assert fibonacci(1) == 1
// @ assert fibonacci(2) == 1
// @ assert fibonacci(3) == 2
}
```

Expand Down Expand Up @@ -237,7 +237,7 @@ To prevent inconsistencies, termination measures must be provided for `pure` fun
pure
ensures res != 0
func incons(x int) (res int) {
return 2 * incons(x)
return 2 * incons(x)
}
```
``` text
Expand All @@ -252,14 +252,14 @@ pure
decreases _ // assuming termination
ensures res != 0
func incons(x int) (res int) {
return 2 * incons(x)
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
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
Expand Down
66 changes: 33 additions & 33 deletions src/termination.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,27 +66,27 @@ We can easily construct a termination measure that decreases instead by subtract
// @ 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
}
}
// @ 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
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.
Expand Down Expand Up @@ -199,23 +199,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)
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
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
}

```
Expand Down

0 comments on commit df91faa

Please sign in to comment.