soma.cell

Counting sort — a non-comparison O(n + k) sort for small non-negative integers, plus the Sieve of Eratosthenes for the primes up to n

Demonstrates: a count array indexed by value, rebuilding the output by emitting each value count-times, and a boolean sieve over a List.

A Soma program from the algorithms part of the verified corpus: 64 lines, cells CountingSort, CountingSortTests. It passes soma check with soma 3.2.4.

How it is built

The cell CountingSort declares 2 signals in its face: sort(xs: List) -> List and primes_upto(n: Int) -> List. Handlers: sort (line 15) and primes_upto (line 29).

The file also holds 1 test cell (CountingSortTests) with 6 assertions, run by soma test.

Generated from soma describe on this file.

The source

counting_sort.cell

// Counting sort — a non-comparison O(n + k) sort for small non-negative
// integers, plus the Sieve of Eratosthenes for the primes up to n.
// Demonstrates: a count array indexed by value, rebuilding the output by
// emitting each value count-times, and a boolean sieve over a List.
//
//   soma run  examples/corpus/algorithms/counting_sort.cell sort "[4,2,2,8,3,3,1]"
//   soma test examples/corpus/algorithms/counting_sort.cell

cell CountingSort {
    face {
        signal sort(xs: List) -> List
        signal primes_upto(n: Int) -> List
    }

    on sort(xs: List) {
        if len(xs) == 0 { return xs }
        let hi = max(xs)
        // counts[v] = how many times v appears
        let counts = list()
        for i in range(0, hi + 1) { counts = push(counts, 0) }
        for v in xs { counts[v] = counts[v] + 1 }
        let out = list()
        for v in range(0, hi + 1) {
            for k in range(0, counts[v]) { out = push(out, v) }
        }
        return out
    }

    on primes_upto(n: Int) {
        if n < 2 { return list() }
        let is_prime = list()
        for i in range(0, n + 1) { is_prime = push(is_prime, true) }
        is_prime[0] = false
        is_prime[1] = false
        let p = 2
        while p * p <= n {
            if is_prime[p] {
                let m = p * p
                while m <= n {
                    is_prime[m] = false
                    m = m + p
                }
            }
            p = p + 1
        }
        let out = list()
        for i in range(2, n + 1) {
            if is_prime[i] { out = push(out, i) }
        }
        return out
    }
}

cell test CountingSortTests {
    rules {
        assert to_string(sort([4, 2, 2, 8, 3, 3, 1])) == to_string([1, 2, 2, 3, 3, 4, 8])
        assert to_string(sort([0, 0, 0])) == to_string([0, 0, 0])
        assert to_string(sort(list())) == to_string(list())
        assert to_string(primes_upto(20)) == to_string([2, 3, 5, 7, 11, 13, 17, 19])
        assert len(primes_upto(100)) == 25
        assert to_string(primes_upto(1)) == to_string(list())
    }
}

What the toolchain says

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ soma check counting_sort.cell
✓ All checks passed.
$ soma test counting_sort.cell
test CountingSortTests ...
  ✓ assert to_string(sort([4, 2, 2, 8, 3, 3, 1])) == to_string([1, 2, 2, 3, 3, 4, 8])
  ✓ assert to_string(sort([0, 0, 0])) == to_string([0, 0, 0])
  ✓ assert to_string(sort(list())) == to_string(list())
  ✓ assert to_string(primes_upto(20)) == to_string([2, 3, 5, 7, 11, 13, 17, 19])
  ✓ assert len(primes_upto(100)) == 25
  ✓ assert to_string(primes_upto(1)) == to_string(list())

6 tests: 6 passed, 0 failed
$ soma verify counting_sort.cell
Verifying counting_sort.cell...

CountingSort/termination:

  ⚠ handler `primes_upto`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)

0 passed, 1 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK
$ soma run counting_sort.cell sort "[4,2,2,8,3,3,1]"
[1, 2, 2, 3, 3, 4, 8]

Builtins used

len, list, max, push, range, to_string

Source file: /corpus/algorithms/counting_sort.cell · examples/corpus/algorithms/counting_sort.cell