Examples

This page walks through several example files to illustrate how perlchecker works in practice.

Basic Verification

File: examples/00_identity_with_pre.pl

# sig: (I64) -> I64
# pre: $x >= 0
# post: $result == $x
sub identity_with_pre {
    my ($x) = @_;
    return $x;
}

$ perlchecker check examples/00_identity_with_pre.pl
✔ identity_with_pre: verified

The function returns its input unchanged. The precondition constrains $x to non-negative values, and the postcondition states the result equals $x. There is one path, and the solver confirms the postcondition holds for all valid inputs.

Finding a Counterexample

File: examples/04_counterexample.pl

# sig: (I64) -> I64
# post: $result > $x
sub counterexample {
    my ($x) = @_;
    if ($x >= 0) {
        return $x;
    } else {
        return $x + 1;
    }
}

$ perlchecker check examples/04_counterexample.pl
✘ counterexample: counterexample found
Function counterexample failed:
  x = 0

The postcondition claims the result is strictly greater than the input. On the $x >= 0 branch, the function returns $x itself — which is not greater than $x. The solver finds x = 0 as a concrete witness.

Safe Division

File: examples/09_safe_division.pl

# sig: (I64, I64) -> I64
# pre: $y != 0
# post: $result == $x / $y
sub safe_division {
    my ($x, $y) = @_;
    return $x / $y;
}

$ perlchecker check examples/09_safe_division.pl
✔ safe_division: verified

The precondition $y != 0 guards against division by zero. The verifier prunes any path where $y == 0, so the division is always safe. Without the precondition, verification would fail because the zero-divisor path would be discarded as invalid, leaving no valid paths to check.

String Operations

File: examples/12_string_concat_length.pl

# sig: (Str, Str) -> Str
# post: length($result) == length($x) + length($y)
sub string_concat_length {
    my ($x, $y) = @_;
    return $x . $y;
}

$ perlchecker check examples/12_string_concat_length.pl
✔ string_concat_length: verified

The postcondition states that concatenating two strings produces a result whose length equals the sum of the input lengths. The Z3 string theory confirms this holds for all strings (up to the 32-character bound).

Arrays

File: examples/21_array_read_verified.pl

# sig: (Array<I64>, I64) -> I64
# post: $result == $arr[$i]
sub array_read_verified {
    my ($arr, $i) = @_;
    return $arr[$i];
}

$ perlchecker check examples/21_array_read_verified.pl
✔ array_read_verified: verified

Arrays are modeled using Z3’s Array theory. Reading an element and returning it trivially satisfies the postcondition $result == $arr[$i].

Function Calls

File: examples/27_function_call_verified.pl

# sig: (I64) -> I64
# post: $result == $x + 1
sub inc {
    my ($x) = @_;
    return $x + 1;
}

# sig: (I64) -> I64
# post: $result == $x + 1
sub function_call_verified {
    my ($x) = @_;
    return inc($x);
}

$ perlchecker check examples/27_function_call_verified.pl
✔ inc: verified
✔ function_call_verified: verified

Both functions are verified. function_call_verified calls inc, which is inlined during verification. The verifier proves that inc($x) returns $x + 1, satisfying the caller’s postcondition.

Loops

File: examples/30_while_verified.pl

# sig: (I64) -> I64
# pre: $x >= 0 && $x <= 5
# post: $result == 0
sub while_verified {
    my ($x) = @_;
    while ($x > 0) {
        $x = $x - 1;
    }
    return $x;
}

$ perlchecker check examples/30_while_verified.pl
✔ while_verified: verified

The precondition bounds $x to [0, 5], ensuring the loop terminates within the default unroll depth of 5. The loop counts down to 0, and the postcondition $result == 0 is verified across all paths.

Note

Without the precondition bounding $x, this function would fail with a “loop unroll bound exceeded” error because the loop could iterate arbitrarily many times.