34. Property Testing

A property is an invariant: a function that must return true for many randomly generated inputs. MALDA draws those inputs from a seed, so the same seed replays the same trials. Use this when a handful of hand-written cases would miss an edge (integers around zero, empty strings, short lists). CLI flags for malda test are summarized in 2. Tools & Tooling; this chapter explains the language construct.

34.1 A property that passes

Declare a property like a function. The body must return a boolean. Same file: Examples/Testing/property_core_identity.malda.

property intIdentity(x) {
    return (x + 0) == x;
}

property boolInvolution(isFlag) {
    return (!(!isFlag)) == isFlag;
}

Run it with a fixed seed so a failure tomorrow is the same failure as today:

malda test Examples/Testing/property_core_identity.malda --iterations 80 --seed 1337

You can also invoke a declared property from ordinary MALDA with runProperty(name, iterations?, seed?):

property stableIdentity(x) {
    return (x + 0) == x;
}

var result = runProperty("stableIdentity", 40, 1337);
print("Passed: " + string(result.passed));

runProperty(...) returns an object with propertyName, passed, iterations, seed, and on failure failedTrial, error, counterexample, shrunkCounterexample.

34.2 How arguments are generated

MALDA does not take explicit generator types. It picks a generator from the parameter name (case-insensitive):

That is why boolInvolution(isFlag) receives booleans and intIdentity(x) receives integers. Rename the parameter if the generator is wrong; there is no property foo(x: string) syntax.

34.3 A property that fails, shrinking, and regressions

When a trial returns false (or throws), MALDA records the arguments as a counterexample, then shrinks them: smaller integers toward zero, shorter strings and lists, until the failure is as small as it can make it. The shrunk payload is what you want in a regression file. Same file: Examples/Testing/property_failure_to_regression.malda.

property alwaysFails(x) {
    return x == (x + 1);
}

var result = runProperty("alwaysFails", 20, 1337);
print("Passed: " + string(result.passed));

# Observe the failure (same seed = same trials)
malda test Examples/Testing/property_failure_to_regression.malda --iterations 40 --seed 1337

# Write a deterministic .spec.malda repro from the shrunk counterexample
malda test Examples/Testing/property_failure_to_regression.malda --iterations 40 --seed 1337 --write-regression

# Optional output directory (default: tests/regressions)
malda test ./tests --write-regression --regression-dir ./artifacts/regressions

# CI JSON for the Desktop IDE "Create Regression" action
malda test ./tests --format ci --iterations 100 --seed 1337

MALDA prints each generated path as Generated regression: .... Desktop Create Regression treats CI paths as untrusted: they are sanitized and clamped to the workspace before any file is written. CI JSON includes shrunkCounterexample, canGenerateRegression, and recommendedRegressionPath.

34.4 Capability model

Properties that need a runtime feature (actors, file I/O, workflows) declare it. A backend that cannot provide the capability is not applicable, not a failure. Same idea: Examples/Testing/property_js_capability_skip.malda.

@requires("core", "actors")
@targets("interpreter", "csharp", "js")
property actorSafetyInvariant(x) {
    return x == x;
}

• @requires(...): capability tags the property needs
• @targets(...): backends where it is expected to run

Supported @requires tags:

• Interpreter: core, file-io, actors, workflows, dotnet-interop, host-interop
• CSharp: core, file-io, actors, workflows, dotnet-interop, host-interop
• JS: core, web-dom, game-canvas

The capability matrix is the source of truth for backend eligibility across interpreter, csharp, and js.

34.5 JavaScript limitations and skip semantics

JavaScript backend parity is capability-gated. If a property requires unsupported JS capabilities, MALDA reports JS as not applicable with a reason. That does not fail parity for the backends that did run.

For JS-eligible properties where a JS property harness is not enabled yet, MALDA reports JS as skipped with an explicit TODO-style reason instead of failing parity.