9e216da9ef
After go1.16, go will use module mode by default, even when the repository is checked out under GOPATH or in a one-off directory. Add go.mod, go.sum to keep this repo buildable without opting out of the module mode. > go mod init github.com/mmcgrana/gobyexample > go mod tidy > go mod vendor In module mode, the 'vendor' directory is special and its contents will be actively maintained by the go command. pygments aren't the dependency the go will know about, so it will delete the contents from vendor directory. Move it to `third_party` directory now. And, vendor the blackfriday package. Note: the tutorial contents are not affected by the change in go1.16 because all the examples in this tutorial ask users to run the go command with the explicit list of files to be compiled (e.g. `go run hello-world.go` or `go build command-line-arguments.go`). When the source list is provided, the go command does not have to compute the build list and whether it's running in GOPATH mode or module mode becomes irrelevant.
141 lines
4.4 KiB
Plaintext
141 lines
4.4 KiB
Plaintext
/*
|
|
* Test Boogie rendering
|
|
*/
|
|
|
|
const N: int;
|
|
axiom 0 <= N;
|
|
|
|
procedure foo() {
|
|
break;
|
|
}
|
|
// array to sort as global array, because partition & quicksort have to
|
|
var a: [int] int;
|
|
var original: [int] int;
|
|
var perm: [int] int;
|
|
|
|
// Is array a of length N sorted?
|
|
function is_sorted(a: [int] int, l: int, r: int): bool
|
|
{
|
|
(forall j, k: int :: l <= j && j < k && k <= r ==> a[j] <= a[k])
|
|
}
|
|
|
|
// is range a[l:r] unchanged?
|
|
function is_unchanged(a: [int] int, b: [int] int, l: int, r: int): bool {
|
|
(forall i: int :: l <= i && i <= r ==> a[i] == b[i])
|
|
}
|
|
|
|
function is_permutation(a: [int] int, original: [int] int, perm: [int] int, N: int): bool
|
|
{
|
|
(forall k: int :: 0 <= k && k < N ==> 0 <= perm[k] && perm[k] < N) &&
|
|
(forall k, j: int :: 0 <= k && k < j && j < N ==> perm[k] != perm[j]) &&
|
|
(forall k: int :: 0 <= k && k < N ==> a[k] == original[perm[k]])
|
|
}
|
|
|
|
function count(a: [int] int, x: int, N: int) returns (int)
|
|
{ if N == 0 then 0 else if a[N-1] == x then count(a, x, N - 1) + 1 else count(a, x, N-1) }
|
|
|
|
|
|
/*
|
|
function count(a: [int] int, x: int, N: int) returns (int)
|
|
{ if N == 0 then 0 else if a[N-1] == x then count(a, x, N - 1) + 1 else count(a, x, N-1) }
|
|
|
|
function is_permutation(a: [int] int, b: [int] int, l: int, r: int): bool {
|
|
(forall i: int :: l <= i && i <= r ==> count(a, a[i], r+1) == count(b, a[i], r+1))
|
|
}
|
|
*/
|
|
|
|
procedure partition(l: int, r: int, N: int) returns (p: int)
|
|
modifies a, perm;
|
|
requires N > 0;
|
|
requires l >= 0 && l < r && r < N;
|
|
requires ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
|
|
requires ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
|
|
|
|
/* a is a permutation of the original array original */
|
|
requires is_permutation(a, original, perm, N);
|
|
|
|
ensures (forall k: int :: (k >= l && k <= p ) ==> a[k] <= a[p]);
|
|
ensures (forall k: int :: (k > p && k <= r ) ==> a[k] > a[p]);
|
|
ensures p >= l && p <= r;
|
|
ensures is_unchanged(a, old(a), 0, l-1);
|
|
ensures is_unchanged(a, old(a), r+1, N);
|
|
ensures ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
|
|
ensures ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
|
|
|
|
/* a is a permutation of the original array original */
|
|
ensures is_permutation(a, original, perm, N);
|
|
{
|
|
var i: int;
|
|
var sv: int;
|
|
var pivot: int;
|
|
var tmp: int;
|
|
|
|
i := l;
|
|
sv := l;
|
|
pivot := a[r];
|
|
|
|
while (i < r)
|
|
invariant i <= r && i >= l;
|
|
invariant sv <= i && sv >= l;
|
|
invariant pivot == a[r];
|
|
invariant (forall k: int :: (k >= l && k < sv) ==> a[k] <= old(a[r]));
|
|
invariant (forall k: int :: (k >= sv && k < i) ==> a[k] > old(a[r]));
|
|
|
|
/* a is a permutation of the original array original */
|
|
invariant is_permutation(a, original, perm, N);
|
|
|
|
invariant is_unchanged(a, old(a), 0, l-1);
|
|
invariant is_unchanged(a, old(a), r+1, N);
|
|
invariant ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
|
|
invariant ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
|
|
{
|
|
if ( a[i] <= pivot) {
|
|
tmp := a[i]; a[i] := a[sv]; a[sv] := tmp;
|
|
tmp := perm[i]; perm[i] := perm[sv]; perm[sv] := tmp;
|
|
sv := sv +1;
|
|
}
|
|
i := i + 1;
|
|
}
|
|
|
|
//swap
|
|
tmp := a[i]; a[i] := a[sv]; a[sv] := tmp;
|
|
tmp := perm[i]; perm[i] := perm[sv]; perm[sv] := tmp;
|
|
|
|
p := sv;
|
|
}
|
|
|
|
|
|
procedure quicksort(l: int, r: int, N: int)
|
|
modifies a, perm;
|
|
|
|
requires N > 0;
|
|
requires l >= 0 && l < r && r < N;
|
|
requires ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
|
|
requires ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
|
|
|
|
/* a is a permutation of the original array original */
|
|
requires is_permutation(a, original, perm, N);
|
|
|
|
ensures ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
|
|
ensures ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
|
|
|
|
ensures is_unchanged(a, old(a), 0, l-1);
|
|
ensures is_unchanged(a, old(a), r+1, N);
|
|
ensures is_sorted(a, l, r);
|
|
|
|
/* a is a permutation of the original array original */
|
|
ensures is_permutation(a, original, perm, N);
|
|
{
|
|
var p: int;
|
|
|
|
call p := partition(l, r, N);
|
|
|
|
if ((p-1) > l) {
|
|
call quicksort(l, p-1, N);
|
|
}
|
|
|
|
if ((p+1) < r) {
|
|
call quicksort(p+1, r, N);
|
|
}
|
|
}
|