This page explains terms that appear throughout the docs, especially in comparisons with other languages and in the mutation and VAST sections.
Verification terms
| Term | Meaning |
|---|
| Preconditions | Rules that must be true before a function runs. In Vary these go in in {}. |
| Postconditions | Rules that must be true after a function returns. In Vary these go in out (result) {}. |
| Invariant | A condition that must always hold for a type or object. In Vary, invariants can be attached to classes and data types. |
old(expr) | The value of an expression at function entry. Used in postconditions to compare before and after state. |
| Design by Contract | A style where code declares its assumptions and guarantees explicitly through preconditions, postconditions, and invariants. |
| Oracle | Anything that tells a test whether behaviour was correct. Assertions, expected outputs, and contracts can all act as oracles. |
| Mutation testing | Testing by injecting small faults and checking whether the test suite notices. In Vary this is built into vary mutate. |
| Surviving mutant | A mutated version of the program that still passes the tests. This usually means the tests did not check something important. |
| Killed mutant | A mutated version of the program that causes a test or contract failure. This means the checks noticed the injected fault. |
| Proof obligation | A condition the compiler or verifier must prove before accepting the program. Common in verification-oriented languages like Dafny. |
| SMT solver | An automated theorem prover used to check logical constraints. Dafny relies on SMT solvers such as Z3 to prove contracts. |
| Ghost code | Verification-only code used to help prove correctness. It does not exist in the final running program. |
| Frame control | A way to declare what state a function is allowed to read or modify. Dafny has reads and modifies; Vary does not. |
| Termination | The guarantee that a function or loop eventually finishes. Some verification languages require explicit proof of this. |
| Differential testing | Testing by running the same program through multiple independent implementations and checking that they agree. This is the core idea behind VAST. |
Language and type-system terms
| Term | Meaning |
|---|
| Static typing | Types are checked before the program runs. Type errors fail during compilation instead of at runtime. |
| Nullable type | A type that may contain no value. In Vary, only T? types can be null. |
| Null safety | Rules that prevent accidental null use unless the type explicitly allows it. |
| Purity | A pure function has no hidden side effects and depends only on its inputs. In Vary, pure def is compiler-enforced. |
| Side effect | Any observable change outside a function's return value, such as writing a file, printing, or mutating shared state. |
| Payload | Data carried by an enum case. For example, Error(message: Str) has a payload. |
| Exhaustive match | A match where every possible case is handled. The compiler checks this for enums. |
| Algebraic data type | A structured type built from named cases and attached data. Vary enums with payloads are in this family of ideas. |
data type | Vary's compact syntax for immutable data-carrying types, similar in spirit to records or dataclasses. |
| Compile time | The stage where source code is analyzed and turned into executable form. |
| Runtime | The stage where the compiled program is actually executing. |
Compiler and runtime terms
| Term | Meaning |
|---|
| Compiler | A program that translates source code into another form that can be executed. |
| Bytecode | A low-level instruction format for a virtual machine. It sits below source code and above raw machine code. |
| JVM bytecode | The instruction format executed by the Java Virtual Machine. Vary compiles to this. |
| Interpreted | Run directly by an interpreter instead of being compiled ahead of time to bytecode or machine code. |
| Classloader | A JVM mechanism for loading classes in isolation. Vary's mutation engine uses isolated classloaders to run mutants safely. |
| Backend | The compiler stage that turns checked program structures into executable output such as JVM bytecode. |
| Code generation | The part of compilation that emits executable instructions. |
| Optimization | Compiler rewrites that preserve meaning while improving speed, size, or structure. |
| Miscompilation | A compiler bug where valid source code is translated into behaviour different from what the program means. |
| AST | Abstract Syntax Tree. A structured representation of the program after parsing. |
| AST interpreter | An engine that executes the parsed program structure directly without first generating bytecode. |
| IR | Intermediate Representation. A compiler-internal form between the parsed program and final output. |
| IR interpreter | An engine that executes the compiler's intermediate form directly. VAST uses this as an independent execution path. |
| Codegen bug | A bug in code generation that produces incorrect executable output. |
How these terms fit in Vary
| Area | Why the terms matter |
|---|
| Comparisons | Pages like Related languages compare Vary to Eiffel, D, Python, and Dafny, so they use verification and type-system terms directly. |
| Mutation docs | Terms like oracle, mutant, survivor, and side effect explain what vary mutate is measuring. |
| VAST docs | Terms like differential testing, AST, IR, and miscompilation explain how VAST checks the compiler itself. |
| Contracts | Terms like precondition, postcondition, invariant, and old(expr) explain how Vary expresses behaviour rules in code. |