Alpha. Vary is under active development and not ready for production use. Syntax, APIs, performance, and behaviour may change between releases.
Glossary
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. |