Some algorithms in Go
- Go 77.4%
- TLA 19.3%
- Makefile 3.3%
| Filename | Latest commit message | Latest commit date |
|---|---|---|
3f906d0326
Extends the verification harness from sorts-only to the whole repo, and in doing so surfaces two further latent bugs (on top of the earlier hash-shift one): Bugs found and fixed: - queue/elementarypriority.go: max() seeded at the zero value, so an all-negative queue reported a phantom max of 0 and DeleteMax returned/removed the wrong element. Caught by the new queue permutation property (testing/quick generates negatives; the old test data never did). Seed from a[0] instead. - sort/sleep.go: result built on NewArrayList(len(a)) -- a slice of that LENGTH (len(a) zeros) -- then appended to, yielding double-length output with leading zeros. The old .Sorted()-only test passed because zeros-then-ascending is sorted. Caught by the new Sleep permutation check. Build from an empty slice. Coverage added: - queue/property_test.go: ordering + permutation (completeness) for both queues. - TestSleepSort now also checks permutation, not just Sorted(). - docs/verification.md: paper proofs for all search/set structures (Elementary, Hash, BST, red-black BST invariants, GoMap) and both priority queues. - formal/tla/ParallelSort.tla: exhaustive fork/join model of ParallelMerge/ ParallelQuick -- disjoint write-ranges (no data race) + termination. Wired into make verify-model. - formal/selection.go: second Gobra proof (memory safety + sortedness). Wired into make verify-formal. - docs/case-study-bugs-found.md: extensive write-up of all three bugs, how each was caught, why the old tests missed it, and the fix (supersedes the earlier single-bug case study). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> |
||
| docs | ||
| ds | ||
| formal | ||
| queue | ||
| search | ||
| sort | ||
| .gitignore | ||
| bench.out | ||
| go.mod | ||
| go.sum | ||
| LICENSE | ||
| Makefile | ||
| README.md | ||
| staticcheck.conf | ||
| test.out | ||
Algorithms
Introduction
This includes exercises from the Algorithms lecture. Well, this is just a refresher exercise.
Testing
For unit tests run:
make test
Benchmarking
For running benchmars run:
make bench