Introduction

Welcome to Pup

Pup is Schematic’s command-line tool for verifying that your code behaves as intended. Supertests describe the required behavior, and Pup uses mathematical reasoning to check whether those requirements hold for every possible input.

Want to follow along?

We’ll write a supertest, use Pup to find a bug, and check the fix. Get started walks you through setup and the example for your language.

These docs adapt to your programming language. Choose yours:

Write a supertest

A supertest looks much like an ordinary unit test: it calls your code and uses assertions to state what should happen. The difference is how it’s checked. A unit test checks specific scenarios. Pup instead reasons about your supertest to check whether its assertions hold for every possible input.

Consider a function that normalizes text by replacing every run of consecutive spaces with one space. Running the function again should leave the normalized text unchanged. We can express that requirement as a supertest:

Consider an 8-bit saturating incrementer. It should add one to its input, stopping at 255. Incrementing a value should never make it smaller. We can express that requirement as a supertest:

from schematic import *

from text_tools.text import collapse_spaces


@supertest
def collapsing_spaces_again_changes_nothing(text: str):
    once = collapse_spaces(text)
    twice = collapse_spaces(once)

    assert twice == once

use schematic::supertest;
use text_tools::collapse_spaces;

#[supertest]
pub fn collapsing_spaces_again_changes_nothing(text: String) {
    let once = collapse_spaces(&text);
    let twice = collapse_spaces(&once);

    assert_eq!(twice, once);
}

#include <assert.h>
#include <schematic.h>
#include <stdlib.h>
#include <string.h>
#include "text.h"

SUPERTEST
void collapsing_spaces_again_changes_nothing(const char *text) {
    SUPERTEST_ASSUME(text != NULL);
    char *once = collapse_spaces(text);
    char *twice = collapse_spaces(once);
    int unchanged = strcmp(twice, once) == 0;

    free(once);
    free(twice);
    assert(unchanged);
}

using Schematic;
using Xunit;

namespace TextTools;

public static class CollapseSpaces
{
    [Supertest]
    public static void CollapsingSpacesAgainChangesNothing(string text)
    {
        string once = Text.CollapseSpaces(text);
        string twice = Text.CollapseSpaces(once);

        Assert.Equal(once, twice);
    }
}

import assert from 'node:assert/strict';
import { assume, supertest } from 'schematic-supertest';
import { collapseSpaces } from '../src/text.js';

export const collapsingSpacesAgainChangesNothing = supertest((text) => {
  assume(typeof text === 'string');
  const once = collapseSpaces(text);
  const twice = collapseSpaces(once);

  assert.equal(twice, once);
});

package texttools;

import static org.junit.Assert.assertEquals;
import static tech.schematic.Assumptions.assume;

import tech.schematic.Supertest;

public final class CollapseSpaces {
    private CollapseSpaces() {}

    @Supertest
    public static void collapsingSpacesAgainChangesNothing(String text) {
        assume(text != null);
        String once = Text.collapseSpaces(text);
        String twice = Text.collapseSpaces(once);

        assertEquals(once, twice);
    }
}

library ieee;
use ieee.numeric_std.all;
use work.incrementer.all;

entity increment_supertests is
  port (value : in natural range 0 to 255);
end entity;

architecture supertests of increment_supertests is
begin
  --% supertest
  increment_never_decreases : process
  begin
    assert to_integer(saturating_increment(to_unsigned(value, 8))) >= value
      report "Increment decreased the value" severity failure;
    wait;
  end process;
end architecture;

In Python, the @supertest decorator tells Pup to treat this test function as a supertest.

In Rust, the #[supertest] attribute tells Pup to treat this test function as a supertest.

In C, SUPERTEST is an empty macro from schematic.h. It tells Pup to treat this function as a supertest without changing how it runs.

In C#, the [Supertest] attribute tells Pup to treat a public static method as a supertest.

In JavaScript, supertest(...) tells Pup to treat this function as a supertest. Assign the result to a named top-level constant. Here, assume restricts the input to strings.

In Java, the @Supertest annotation tells Pup to treat a public static method as a supertest.

The comment --% supertest tells Pup to treat the following labeled process as a supertest. The process label is the supertest name, and the enclosing entity’s input ports define its inputs.

A supertest can take parameters to describe a requirement across a range of inputs. Here, text represents every possible string, not just a few examples. That includes easy-to-miss cases such as empty strings, strings without spaces, and long runs of spaces. Pup checks whether the assertion holds by reasoning about the code, rather than running the supertest on inputs one by one.

The input port value covers every integer from 0 through 255. Pup reasons about the code to check whether the assertion holds across that entire range.

Check the supertest with Pup

Start a check by passing the supertest file to Pup:

$ pup check supertests/collapse_spaces.py
  ⠋ checking · collapsing_spaces_again_changes_nothing
  supertests/collapse_spaces.py:6 · 8e44bea · #1

   Sniffing... Beginning direct analysis of the claim and code.
   Elapsed 3s · last update 0s ago

  Esc/Ctrl+C detach

$ pup check tests/collapse_spaces.rs
  ⠋ checking · collapsing_spaces_again_changes_nothing
  tests/collapse_spaces.rs:4 · 8e44bea · #1

   Sniffing... Beginning direct analysis of the claim and code.
   Elapsed 3s · last update 0s ago

  Esc/Ctrl+C detach

$ pup check supertests/collapse_spaces.c
  ⠋ checking · collapsing_spaces_again_changes_nothing
  supertests/collapse_spaces.c:7 · 8e44bea · #1

   Sniffing... Beginning direct analysis of the claim and code.
   Elapsed 3s · last update 0s ago

  Esc/Ctrl+C detach

$ pup check supertests/CollapseSpaces.cs
  ⠋ checking · CollapsingSpacesAgainChangesNothing
  supertests/CollapseSpaces.cs:8 · 8e44bea · #1

   Sniffing... Beginning direct analysis of the claim and code.
   Elapsed 3s · last update 0s ago

  Esc/Ctrl+C detach

$ pup check supertests/collapse_spaces.js
  ⠋ checking · collapsingSpacesAgainChangesNothing
  supertests/collapse_spaces.js:5 · 8e44bea · #1

   Sniffing... Beginning direct analysis of the claim and code.
   Elapsed 3s · last update 0s ago

  Esc/Ctrl+C detach

$ pup check src/test/java/texttools/CollapseSpaces.java
  ⠋ checking · collapsingSpacesAgainChangesNothing
  src/test/java/texttools/CollapseSpaces.java:11 · 8e44bea · #1

   Sniffing... Beginning direct analysis of the claim and code.
   Elapsed 3s · last update 0s ago

  Esc/Ctrl+C detach

$ pup check supertests/increment.vhd
  ⠋ checking · increment_never_decreases
  supertests/increment.vhd:11 · 8e44bea · #1

   Sniffing... Beginning direct analysis of the claim and code.
   Elapsed 3s · last update 0s ago

  Esc/Ctrl+C detach

Pup shows activity while checking and keeps the results open for you to review. When the check finishes, Pup reports whether the supertest passed or failed.

Here, it fails: the counterexample is a string with three spaces between a and b. One counterexample is enough to show that the requirement doesn’t always hold. Once the fix proposal arrives, the result includes a command to review it:

Here, it fails: input 255 produces 0, which is smaller than the input. One counterexample is enough to show that the requirement doesn’t always hold. Once the fix proposal arrives, the result includes a command to review it:

  × fail · collapsing_spaces_again_changes_nothing
  supertests/collapse_spaces.py:6 · 8e44bea · #1

   Collapsing spaces again changes the text.

   A single replacement can leave adjacent spaces.

   Counterexample
   witness  = text = "a   b"
   expected = the second call returns the same text as the first
   observed = first call: "a  b"; second call: "a b"

   Review and apply: pup fix --check 1

  Enter for more details · Esc/Ctrl+C close

  × fail · collapsing_spaces_again_changes_nothing
  tests/collapse_spaces.rs:4 · 8e44bea · #1

   Collapsing spaces again changes the text.

   A single replacement can leave adjacent spaces.

   Counterexample
   witness  = text = "a   b"
   expected = the second call returns the same text as the first
   observed = first call: "a  b"; second call: "a b"

   Review and apply: pup fix --check 1

  Enter for more details · Esc/Ctrl+C close

  × fail · collapsing_spaces_again_changes_nothing
  supertests/collapse_spaces.c:7 · 8e44bea · #1

   Collapsing spaces again changes the text.

   A single replacement can leave adjacent spaces.

   Counterexample
   witness  = text = "a   b"
   expected = the second call returns the same text as the first
   observed = first call: "a  b"; second call: "a b"

   Review and apply: pup fix --check 1

  Enter for more details · Esc/Ctrl+C close

  × fail · CollapsingSpacesAgainChangesNothing
  supertests/CollapseSpaces.cs:8 · 8e44bea · #1

   Collapsing spaces again changes the text.

   A single replacement can leave adjacent spaces.

   Counterexample
   witness  = text = "a   b"
   expected = the second call returns the same text as the first
   observed = first call: "a  b"; second call: "a b"

   Review and apply: pup fix --check 1

  Enter for more details · Esc/Ctrl+C close

  × fail · collapsingSpacesAgainChangesNothing
  supertests/collapse_spaces.js:5 · 8e44bea · #1

   Collapsing spaces again changes the text.

   A single replacement can leave adjacent spaces.

   Counterexample
   witness  = text = "a   b"
   expected = the second call returns the same text as the first
   observed = first call: "a  b"; second call: "a b"

   Review and apply: pup fix --check 1

  Enter for more details · Esc/Ctrl+C close

  × fail · collapsingSpacesAgainChangesNothing
  src/test/java/texttools/CollapseSpaces.java:11 · 8e44bea · #1

   Collapsing spaces again changes the text.

   A single replacement can leave adjacent spaces.

   Counterexample
   witness  = text = "a   b"
   expected = the second call returns the same text as the first
   observed = first call: "a  b"; second call: "a b"

   Review and apply: pup fix --check 1

  Enter for more details · Esc/Ctrl+C close

  × fail · increment_never_decreases
  supertests/increment.vhd:11 · 8e44bea · #1

   Incrementing 255 decreases the value.

   An 8-bit addition wraps from 255 to zero.

   Counterexample
   witness  = value = 255
   expected = the result is at least 255
   observed = the result is 0

   Review and apply: pup fix --check 1

  Enter for more details · Esc/Ctrl+C close

Fix the implementation and check again

Review and apply Pup’s proposed fix with pup fix:

$ pup fix --check 1
  supertest-python · 8e44bea
  Fix proposal · collapsing_spaces_again_changes_nothing · #1
  Repeat the replacement until no consecutive spaces remain.

  text_tools/text.py  +3 -1
  old new   @@ -1,2 +1,4 @@
    1   1   def collapse_spaces(text: str) -> str:
    2     -     return text.replace("  ", " ")
        2 +     while "  " in text:
        3 +         text = text.replace("  ", " ")
        4 +     return text

  ? Apply this fix to your working tree? [Y/n] › yes

  ✓ Applied · 1 file changed
  Changes are uncommitted.

  Next: pup check supertests/collapse_spaces.py::collapsing_spaces_again_changes_nothing

$ pup fix --check 1
  supertest-rust · 8e44bea
  Fix proposal · collapsing_spaces_again_changes_nothing · #1
  Repeat the replacement until no consecutive spaces remain.

  src/text.rs  +5 -1
  old new   @@ -1,3 +1,7 @@
    1   1   pub fn collapse_spaces(text: &str) -> String {
    2     -     text.replace("  ", " ")
        2 +     let mut normalized = text.to_owned();
        3 +     while normalized.contains("  ") {
        4 +         normalized = normalized.replace("  ", " ");
        5 +     }
        6 +     normalized
    3   7   }

  ? Apply this fix to your working tree? [Y/n] › yes

  ✓ Applied · 1 file changed
  Changes are uncommitted.

  Next: pup check tests/collapse_spaces.rs::collapsing_spaces_again_changes_nothing

$ pup fix --check 1
  supertest-c · 8e44bea
  Fix proposal · collapsing_spaces_again_changes_nothing · #1
  Skip the rest of each run of spaces by changing if to while.

  src/text.c  +1 -1
  old new   @@ -11,7 +11,7 @@
   11  11       char *dst = normalized;
   12  12       for (const char *src = text; *src != '\0'; ++src) {
   13  13           *dst++ = *src;
   14     -         if (*src == ' ' && src[1] == ' ') {
       14 +         while (*src == ' ' && src[1] == ' ') {
   15  15               ++src;
   16  16           }
   17  17       }

  ? Apply this fix to your working tree? [Y/n] › yes

  ✓ Applied · 1 file changed
  Changes are uncommitted.

  Next: pup check supertests/collapse_spaces.c::collapsing_spaces_again_changes_nothing

$ pup fix --check 1
  supertest-csharp · 8e44bea
  Fix proposal · CollapsingSpacesAgainChangesNothing · #1
  Repeat the replacement until no consecutive spaces remain.

  Text.cs  +5 -1
  old new   @@ -4,6 +4,10 @@

    4   4   {
    5   5       public static string CollapseSpaces(string text)
    6   6       {
    7     -         return text.Replace("  ", " ");
        7 +         while (text.Contains("  "))
        8 +         {
        9 +             text = text.Replace("  ", " ");
       10 +         }
       11 +         return text;
    8  12       }
    9  13   }

  ? Apply this fix to your working tree? [Y/n] › yes

  ✓ Applied · 1 file changed
  Changes are uncommitted.

  Next: pup check supertests/CollapseSpaces.cs::CollapsingSpacesAgainChangesNothing

$ pup fix --check 1
  supertest-javascript · 8e44bea
  Fix proposal · collapsingSpacesAgainChangesNothing · #1
  Replace each complete run of spaces with one space.

  src/text.js  +1 -1
  old new   @@ -1,3 +1,3 @@

    1   1   export function collapseSpaces(text) {
    2     -   return text.replaceAll('  ', ' ');
        2 +   return text.replace(/ +/g, ' ');
    3   3   }

  ? Apply this fix to your working tree? [Y/n] › yes

  ✓ Applied · 1 file changed
  Changes are uncommitted.

  Next: pup check supertests/collapse_spaces.js::collapsingSpacesAgainChangesNothing

$ pup fix --check 1
  supertest-java · 8e44bea
  Fix proposal · collapsingSpacesAgainChangesNothing · #1
  Replace each complete run of spaces with one space.

  src/main/java/texttools/Text.java  +1 -1
  old new   @@ -4,6 +4,6 @@

    4   4       private Text() {}
    5   5
    6   6       public static String collapseSpaces(String text) {
    7     -         return text.replace("  ", " ");
        7 +         return text.replaceAll(" +", " ");
    8   8       }
    9   9   }

  ? Apply this fix to your working tree? [Y/n] › yes

  ✓ Applied · 1 file changed
  Changes are uncommitted.

  Next: pup check src/test/java/texttools/CollapseSpaces.java::collapsingSpacesAgainChangesNothing

$ pup fix --check 1
  supertest-vhdl · 8e44bea
  Fix proposal · increment_never_decreases · #1
  Return 255 unchanged and increment smaller values normally.

  src/incrementer.vhd  +3 -0
  old new   @@ -9,6 +9,9 @@

    9   9   package body incrementer is
   10  10     function saturating_increment(value : byte_value) return byte_value is
   11  11     begin
       12 +     if value = 255 then
       13 +       return value;
       14 +     end if;
   12  15       return value + 1;
   13  16     end function;
   14  17   end package body;

  ? Apply this fix to your working tree? [Y/n] › yes

  ✓ Applied · 1 file changed
  Changes are uncommitted.

  Next: pup check supertests/increment.vhd::increment_never_decreases

Check the updated code with pup check:

$ pup check supertests/collapse_spaces.py::collapsing_spaces_again_changes_nothing
  ? Uncommitted changes found. Proceed with the check, including these changes?
  [Y/n] › yes

  collapsing_spaces_again_changes_nothing

  Check history
    STATUS · COMMIT  · CHECK · REQUESTED
  › ✓ pass · c2f19a6 · #2    · 1m ago
    × fail · 8e44bea · #1    · 4m ago

   supertests/collapse_spaces.py:6 · uncommitted changes · based on 8e44bea

   Normalization reaches a fixed point.

  ↑/↓ attempts · Enter for more details · Esc/Ctrl+C close

$ pup check tests/collapse_spaces.rs::collapsing_spaces_again_changes_nothing
  ? Uncommitted changes found. Proceed with the check, including these changes?
  [Y/n] › yes

  collapsing_spaces_again_changes_nothing

  Check history
    STATUS · COMMIT  · CHECK · REQUESTED
  › ✓ pass · c2f19a6 · #2    · 1m ago
    × fail · 8e44bea · #1    · 4m ago

   tests/collapse_spaces.rs:4 · uncommitted changes · based on 8e44bea

   Normalization reaches a fixed point.

  ↑/↓ attempts · Enter for more details · Esc/Ctrl+C close

$ pup check supertests/collapse_spaces.c::collapsing_spaces_again_changes_nothing
  ? Uncommitted changes found. Proceed with the check, including these changes?
  [Y/n] › yes

  collapsing_spaces_again_changes_nothing

  Check history
    STATUS · COMMIT  · CHECK · REQUESTED
  › ✓ pass · c2f19a6 · #2    · 1m ago
    × fail · 8e44bea · #1    · 4m ago

   supertests/collapse_spaces.c:7 · uncommitted changes · based on 8e44bea

   Normalization reaches a fixed point.

  ↑/↓ attempts · Enter for more details · Esc/Ctrl+C close

$ pup check supertests/CollapseSpaces.cs::CollapsingSpacesAgainChangesNothing
  ? Uncommitted changes found. Proceed with the check, including these changes?
  [Y/n] › yes

  CollapsingSpacesAgainChangesNothing

  Check history
    STATUS · COMMIT  · CHECK · REQUESTED
  › ✓ pass · c2f19a6 · #2    · 1m ago
    × fail · 8e44bea · #1    · 4m ago

   supertests/CollapseSpaces.cs:8 · uncommitted changes · based on 8e44bea

   Normalization reaches a fixed point.

  ↑/↓ attempts · Enter for more details · Esc/Ctrl+C close

$ pup check supertests/collapse_spaces.js::collapsingSpacesAgainChangesNothing
  ? Uncommitted changes found. Proceed with the check, including these changes?
  [Y/n] › yes

  collapsingSpacesAgainChangesNothing

  Check history
    STATUS · COMMIT  · CHECK · REQUESTED
  › ✓ pass · c2f19a6 · #2    · 1m ago
    × fail · 8e44bea · #1    · 4m ago

   supertests/collapse_spaces.js:5 · uncommitted changes · based on 8e44bea

   Normalization reaches a fixed point.

  ↑/↓ attempts · Enter for more details · Esc/Ctrl+C close

$ pup check src/test/java/texttools/CollapseSpaces.java::collapsingSpacesAgainChangesNothing
  ? Uncommitted changes found. Proceed with the check, including these changes?
  [Y/n] › yes

  collapsingSpacesAgainChangesNothing

  Check history
    STATUS · COMMIT  · CHECK · REQUESTED
  › ✓ pass · c2f19a6 · #2    · 1m ago
    × fail · 8e44bea · #1    · 4m ago

   src/test/java/texttools/CollapseSpaces.java:11 · uncommitted changes · based on 8e44bea

   Normalization reaches a fixed point.

  ↑/↓ attempts · Enter for more details · Esc/Ctrl+C close

$ pup check supertests/increment.vhd::increment_never_decreases
  ? Uncommitted changes found. Proceed with the check, including these changes?
  [Y/n] › yes

  increment_never_decreases

  Check history
    STATUS · COMMIT  · CHECK · REQUESTED
  › ✓ pass · c2f19a6 · #2    · 1m ago
    × fail · 8e44bea · #1    · 4m ago

   supertests/increment.vhd:11 · uncommitted changes · based on 8e44bea

   Incrementing never decreases the value.

  ↑/↓ attempts · Enter for more details · Esc/Ctrl+C close

The supertest now passes. Pup has verified that collapsing spaces a second time leaves the result unchanged for every possible string.

The supertest now passes. Pup has verified that incrementing never decreases the value for any input from 0 through 255.

Why use supertests

A single supertest can express the requirement behind many individual test cases. Pup can use mathematical reasoning to prove that the requirement holds for every possible input, or find a counterexample that shows why it doesn’t. As the code changes, the same supertest can be checked again to verify that the requirement still holds.

Next steps

Get started walks you through installation and your first check. Learn more about writing supertests or see the pup check command reference.

Welcome to Pup

Write a supertest#

Check the supertest with Pup#

Fix the implementation and check again#

Why use supertests#

Next steps#

Write a supertest

Check the supertest with Pup

Fix the implementation and check again

Why use supertests

Next steps