# Correctness / Determinism / Verification

> Every term in this category is listed as one record, with its kind, its definition and its aliases, the principles whose relations name it, the principle or…

Page: Ontology · Lexicon
Canonical: https://banes-lab.com/ontology/lexicon#lex-category-correctness-determinism-verification

Every term in this category is listed as one record, with its kind, its definition and its aliases, the principles whose relations name it, the principle or contract that carries the same name where one exists, and the layer its category belongs to.

### Allocation Cost

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree of extra memory allocation incurred by creating new immutable values instead of mutating in place.

Referenced by
[Immutability](https://banes-lab.com/records/arch/immutability.md)

### Assumption-Driven Delivery

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Shipping on untested assumptions about behavior instead of validating that requirements are met.

Referenced by
[Validation](https://banes-lab.com/records/arch/validation.md)

### Behavior Validation

- Kind: [capability](https://banes-lab.com/records/kind/capability.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The ability to confirm a system behaves as its specification requires.

Referenced by
[Specification-Based Testing](https://banes-lab.com/records/arch/specification-based-testing.md)

### Broad Input Exploration

- Kind: [capability](https://banes-lab.com/records/kind/capability.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The ability to exercise a function across a wide, generated range of inputs.

Referenced by
[Property-Based Testing](https://banes-lab.com/records/arch/property-based-testing.md)

### Continuous Updates

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree to which pinning everything for reproducibility conflicts with continuously updating dependencies.

Referenced by
[Reproducibility](https://banes-lab.com/records/arch/reproducibility.md)

### Controlled State

- Kind: [constraint](https://banes-lab.com/records/kind/constraint.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The requirement that all inputs and state affecting a computation be controlled and known.

Referenced by
[Determinism](https://banes-lab.com/records/arch/determinism.md)

### Cost/Complexity

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree of cost and complexity added by formally proving a system correct.

Referenced by
[Formal Verification](https://banes-lab.com/records/arch/formal-verification.md)

### Deterministic Behavior

- Kind: [constraint](https://banes-lab.com/records/kind/constraint.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The requirement that the code under test produce the same result for the same inputs.

Referenced by
[Testability](https://banes-lab.com/records/arch/testability.md)

### Dynamic Runtime Behavior

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree to which runtime-adaptive behavior undermines a system's predictability.

Referenced by
[Predictability](https://banes-lab.com/records/arch/predictability.md)

### Encapsulation Extremes

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree to which hiding internals too strictly makes a unit's behavior hard to observe in tests.

Referenced by
[Testability](https://banes-lab.com/records/arch/testability.md)

### Environment-Sensitive Behavior

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Behavior that changes with the host environment, so the same run yields different results elsewhere.

Referenced by
[Repeatability](https://banes-lab.com/records/arch/repeatability.md)

### Example-Only Testing

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Testing only a few hand-picked examples instead of properties that must hold across all inputs.

Referenced by
[Property-Based Testing](https://banes-lab.com/records/arch/property-based-testing.md)

### Fitness for Use

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree to which a product meets the needs of its users.

Referenced by
[Validation](https://banes-lab.com/records/arch/validation.md)

### Floating Dependencies

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Depending on unpinned, floating dependency versions, so builds are not reproducible.

Referenced by
[Reproducibility](https://banes-lab.com/records/arch/reproducibility.md)

### Formal Specification

- Kind: [artifact](https://banes-lab.com/records/kind/artifact.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
A precise, mathematical statement of what a system must do, against which it is proven.

Referenced by
[Formal Verification](https://banes-lab.com/records/arch/formal-verification.md)

### Hidden Behavior

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Behavior triggered by hidden state or side effects, so outcomes surprise callers.

Referenced by
[Predictability](https://banes-lab.com/records/arch/predictability.md)

### Hidden IO

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Performing input/output inside a supposedly pure function, hiding side effects from callers.

Referenced by
[Pure Functions](https://banes-lab.com/records/arch/pure-functions.md)

### Hidden Time/Randomness/Global State

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Reading the clock, randomness, or global state inside a computation, making its output nondeterministic.

Referenced by
[Determinism](https://banes-lab.com/records/arch/determinism.md)

### Implementation-Only Testing

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Testing only against the current implementation's behavior rather than the specified contract.

Referenced by
[Specification-Based Testing](https://banes-lab.com/records/arch/specification-based-testing.md)

### Informal Validation Only

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Relying only on informal checks and testing where a formal proof of correctness is warranted.

Referenced by
[Formal Verification](https://banes-lab.com/records/arch/formal-verification.md)

### Mathematical Assurance

- Kind: [capability](https://banes-lab.com/records/kind/capability.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The ability to prove mathematically that a system meets its specification.

Referenced by
[Formal Verification](https://banes-lab.com/records/arch/formal-verification.md)

### No Side Effects

- Kind: [constraint](https://banes-lab.com/records/kind/constraint.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The requirement that a function compute its result without observable side effects.

Referenced by
[Pure Functions](https://banes-lab.com/records/arch/pure-functions.md)

### Properties/Invariants

- Kind: [constraint](https://banes-lab.com/records/kind/constraint.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The requirement that the general properties or invariants a function must satisfy be defined.

Referenced by
[Property-Based Testing](https://banes-lab.com/records/arch/property-based-testing.md)

### Real-World Variability

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree to which controlling conditions for repeatability diverges from real-world variability.

Referenced by
[Repeatability](https://banes-lab.com/records/arch/repeatability.md)

### Regression Safety

- Kind: [capability](https://banes-lab.com/records/kind/capability.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The ability to catch regressions when code changes by re-running tests.

Referenced by
[Testability](https://banes-lab.com/records/arch/testability.md)

### Reliable Automation

- Kind: [capability](https://banes-lab.com/records/kind/capability.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The ability to automate a process reliably because it repeats identically each run.

Referenced by
[Repeatability](https://banes-lab.com/records/arch/repeatability.md)

### Reliable Testing

- Kind: [capability](https://banes-lab.com/records/kind/capability.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The ability to test dependably because the same inputs always produce the same outputs.

Referenced by
[Determinism](https://banes-lab.com/records/arch/determinism.md)

### Ruleset

- Kind: [artifact](https://banes-lab.com/records/kind/artifact.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The set of rules a static analyzer checks source code against.

Referenced by
[Static Analysis](https://banes-lab.com/records/arch/static-analysis.md)

### Runtime Adaptivity

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree to which making behavior deterministic limits adapting dynamically at runtime.

Referenced by
[Determinism](https://banes-lab.com/records/arch/determinism.md)

### Safe Operation

- Kind: [capability](https://banes-lab.com/records/kind/capability.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The ability to operate without producing incorrect or harmful results.

Referenced by
[Correctness](https://banes-lab.com/records/arch/correctness.md)

### Safe Sharing

- Kind: [capability](https://banes-lab.com/records/kind/capability.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The ability to share data freely across threads because it cannot be modified.

Referenced by
[Immutability](https://banes-lab.com/records/arch/immutability.md)

### Shrinking/Debug Complexity

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree to which reducing a failing generated case to a minimal example adds debugging complexity.

Referenced by
[Property-Based Testing](https://banes-lab.com/records/arch/property-based-testing.md)

### Side Effects

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Producing observable side effects in an expression, so it cannot be replaced by its value.

Referenced by
[Referential Transparency](https://banes-lab.com/records/arch/referential-transparency.md)

### Spec Maintenance

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree of ongoing effort to keep a specification current as the system evolves.

Referenced by
[Specification-Based Testing](https://banes-lab.com/records/arch/specification-based-testing.md)

### Specification Compliance

- Kind: [capability](https://banes-lab.com/records/kind/capability.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The ability to confirm an implementation conforms to its specification.

Referenced by
[Verification](https://banes-lab.com/records/arch/verification.md)

### Stateful IO

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree to which stateful input/output conflicts with expressions being replaceable by their values.

Referenced by
[Referential Transparency](https://banes-lab.com/records/arch/referential-transparency.md)

### Stateful Operations

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree to which operations that depend on or mutate state conflict with purity.

Referenced by
[Pure Functions](https://banes-lab.com/records/arch/pure-functions.md)

### Tests

- Kind: [artifact](https://banes-lab.com/records/kind/artifact.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Executable checks that assert a system behaves as intended.

Referenced by
[Correctness](https://banes-lab.com/records/arch/correctness.md)

### Thread Safety

- Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The degree to which data can be accessed concurrently without corruption.

Referenced by
[Immutability](https://banes-lab.com/records/arch/immutability.md)

### Unchecked Dynamic Code

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Running dynamically generated or evaluated code that static analysis cannot inspect for defects.

Referenced by
[Static Analysis](https://banes-lab.com/records/arch/static-analysis.md)

### Undefined Behavior

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Relying on operations whose result is unspecified, so outcomes vary unpredictably across runs or platforms.

Referenced by
[Correctness](https://banes-lab.com/records/arch/correctness.md)

### Untested Implementation

- Kind: [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
Shipping code with no tests, so its conformance to the specification is unverified.

Referenced by
[Verification](https://banes-lab.com/records/arch/verification.md)

### Value Semantics

- Kind: [constraint](https://banes-lab.com/records/kind/constraint.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The requirement that values be compared and copied by content rather than by reference identity.

Referenced by
[Immutability](https://banes-lab.com/records/arch/immutability.md)

### Versioned Inputs

- Kind: [constraint](https://banes-lab.com/records/kind/constraint.md)
- Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lex-category-correctness-determinism-verification.md)
- Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)

Details

Definition
The requirement that all inputs to a build or computation be pinned to specific versions.

Referenced by
[Reproducibility](https://banes-lab.com/records/arch/reproducibility.md)

## Links to

- [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md)
- [Computation Core](https://banes-lab.com/records/layer/computation-core.md)
- [Immutability](https://banes-lab.com/records/arch/immutability.md)
- [anti-pattern](https://banes-lab.com/records/kind/anti-pattern.md)
- [Validation](https://banes-lab.com/records/arch/validation.md)
- [capability](https://banes-lab.com/records/kind/capability.md)
- [Specification-Based Testing](https://banes-lab.com/records/arch/specification-based-testing.md)
- [Property-Based Testing](https://banes-lab.com/records/arch/property-based-testing.md)
- [Reproducibility](https://banes-lab.com/records/arch/reproducibility.md)
- [constraint](https://banes-lab.com/records/kind/constraint.md)
- [Determinism](https://banes-lab.com/records/arch/determinism.md)
- [Formal Verification](https://banes-lab.com/records/arch/formal-verification.md)
- [Testability](https://banes-lab.com/records/arch/testability.md)
- [Predictability](https://banes-lab.com/records/arch/predictability.md)
- [Repeatability](https://banes-lab.com/records/arch/repeatability.md)
- [artifact](https://banes-lab.com/records/kind/artifact.md)
- [Pure Functions](https://banes-lab.com/records/arch/pure-functions.md)
- [Static Analysis](https://banes-lab.com/records/arch/static-analysis.md)
- [Correctness](https://banes-lab.com/records/arch/correctness.md)
- [Referential Transparency](https://banes-lab.com/records/arch/referential-transparency.md)
- [Verification](https://banes-lab.com/records/arch/verification.md)
