diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 24 |
1 files changed, 24 insertions, 0 deletions
@@ -1,6 +1,30 @@ test: go clean -testcache go test ./... -v + +# verify: static + dynamic correctness checks. Fast enough for routine use. +# go vet / staticcheck - static analysis +# go test -race -short - race detector over the (size-capped) test + property +# suites; -short keeps the million-element cases out so +# the race build stays quick. See docs/verification.md. +verify: + go vet ./... + staticcheck ./... + go test -race -short ./... + +# verify-model: exhaustively model-check the concurrent sleep sort with TLA+/TLC +# (a model of sort/sleep.go, not the Go code itself). See formal/tla/README.md. +verify-model: + java -cp $(HOME)/tools/tlaplus/tla2tools.jar tlc2.TLC -workers auto \ + -metadir /tmp/tlc-algorithms \ + -config formal/tla/SleepSort.cfg formal/tla/SleepSort.tla + +# verify-formal: machine-checked deductive proof of a monomorphized insertion +# sort with Gobra (Go verifier, Viper+Z3 backend), run from its container image. +# See formal/README.md. +verify-formal: + podman run --rm -v $(PWD)/formal:/gobra/formal:z \ + ghcr.io/viperproject/gobra:latest -i /gobra/formal/insertion.go bench: go test -run=xxx -bench=. ./... | tee bench.out sortbench: |