Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

SSPUR in 5 minutes

This page goes from hello world to a function whose contract is fuzzed and proved. It assumes sspur is installed (Installation), or you can try it in the playground first, which runs the programs in your browser. Every file and terminal session here is a real file under docs/snippets/get-started/, and CI runs each command against the current compiler.

Hello, world

Save this as hello.ssp:

fn main() -> Unit ! log
= log("hello, world")

$ sspur run hello.ssp
hello, world

fn main() -> Unit ! log says that main returns nothing and performs one effect, log. The body comes after =. If main also wrote a file or read the clock, the checker would refuse the program until the signature said so.

A function with a contract

Save this as price.ssp:

// Apply a percentage discount to a price in cents.
fn discount(price: Int, pct: Int) -> Int
  pre price >= 0 and pct >= 0 and pct <= 100
  post r >= 0 and r <= price
= price - price * pct / 100

fn main() -> Unit ! log
= log("a 2000 cent book at 15% off costs {discount(2000, 15)}")

test half_off = discount(1000, 50) == 500
test no_discount = discount(999, 0) == 999
test free = discount(10, 100) == 0

pre is what callers must guarantee and post is what the function promises about its result r. Both are checked every time the function runs. "{discount(2000, 15)}" puts an expression’s value into a string, and a test is a named Bool expression.

$ sspur run price.ssp
a 2000 cent book at 15% off costs 1700
$ sspur test price.ssp
3 passed, 0 failed

Fuzz it, then prove it

You wrote the contract once, and SSPUR uses it twice more. sspur fuzz generates arguments that satisfy pre and checks post on every result. sspur verify hands the contracts to Z3 and tries to prove them for all inputs:

$ sspur fuzz price.ssp
ok    discount (200 cases, 1210 discarded)
skip  main (no parameters)
$ sspur verify price.ssp
fn discount
  pre price >= 0 and pct >= 0 and pct <= 100   proved: at 4 call sites
  post r >= 0 and r <= price                   proved
2 proved, 0 counterexample, 0 unknown; 3 of 4 runtime checks proved safe

verify proved the postcondition, proved that all 4 calls in the file meet the precondition, and found that 3 of the 4 runtime checks can never fail, so native code leaves them out.

Now break the contract. Save a copy as price_bug.ssp that claims a discount always lowers the price:

  post r < price

$ sspur fuzz price_bug.ssp
FAIL  discount(0, 0): contract violated: post r < price in discount (r = 0)
skip  main (no parameters)

The fuzzer found the counterexample: a price of 0 with no discount stays 0.

Records and pattern matching

type Point = {x: Int, y: Int}

type Shape = Circle{center: Point, r: Int where _ > 0} | Rect{corner: Point, w: Int, h: Int} | Dot

fn area(s: Shape) -> Int
= match s
  | Circle{r} => 3 * r * r
  | Rect{w, h} => w * h
  | Dot => 0

fn describe(s: Shape) -> Str
= match s
  | Circle{center, r} => "circle at ({center.x}, {center.y}), radius {r}"
  | Rect{w, h} if w == h => "square {w}x{h}"
  | Rect{w, h} => "rect {w}x{h}"
  | Dot => "dot"

fn main() -> Unit ! log
= do
  origin = Point{x: 0, y: 0}
  shapes = [Circle{center: origin, r: 2}, Rect{corner: origin, w: 3, h: 3}, Rect{corner: origin with x := 5, w: 4, h: 1}, Dot]
  for s in shapes
    log("{describe(s)}: area {area(s)}")
  log("total area {shapes.map(area).sum}")

test square = describe(Rect{corner: Point{x: 1, y: 1}, w: 2, h: 2}) == "square 2x2"
test dot_area = area(Dot) == 0

Point is a record and Shape a sum type with three variants. match must cover every variant, or the checker names the missing one. Circle{r} binds only the fields it names, if w == h is a guard, and origin with x := 5 is a copy of origin with one field changed. Values never change in place.

$ sspur run shapes.ssp
circle at (0, 0), radius 2: area 12
square 3x3: area 9
rect 4x1: area 4
dot: area 0
total area 25
$ sspur test shapes.ssp
2 passed, 0 failed

Where next