Glossary¶

Terms as used in the KYLLO documentation. Definitions are drawn from the source material; each entry cites its authoritative section. Where the source leaves a term partly undefined, the entry says so.

Contract¶

A declared requirement on a function or type: its preconditions, postconditions, invariants, effects, and failure conditions. Every function must explicitly declare its contract.

Source: language-guide/functions.md, technical-specification/TECHSPEC-03.md.

Precondition (`REQUIRES`)¶

What must be true before a function executes. Preconditions must be checked or established by the caller.

Source: technical-specification/TECHSPEC-03.md.

Postcondition (`ENSURES`)¶

What must be true after successful execution. Successful execution must satisfy the declared postconditions.

Source: technical-specification/TECHSPEC-03.md.

Invariant (`INVARIANT`)¶

A condition that must hold throughout the lifetime of a value or type, e.g. balance >= 0 for an account.

Source: getting-started/first-program.md, technical-specification/TECHSPEC-03.md.

`OLD`¶

Refers to the previous state of a value in a postcondition, e.g. result.balance == OLD(account.balance) + amount.

Source: technical-specification/TECHSPEC-03.md.

`Result`¶

A safety type representing either success (the expected return value) or a declared failure. Operations that can fail must return an explicit Result.

Source: language-guide/types.md, language-guide/error-handling.md, technical-specification/TECHSPEC-10.md.

`Optional`¶

A safety type representing a value that may be absent. The compiler must require the absence case to be handled before accessing the contained value.

Source: language-guide/types.md, technical-specification/TECHSPEC-24.md.

`NonNull`¶

A safety type: a value that cannot be null.

Source: language-guide/types.md.

`Bounded`¶

A safety type: a numeric value constrained by declared limits.

Source: language-guide/types.md.

`Validated`¶

A safety type: a value that has passed specified validation rules.

Source: language-guide/types.md.

Effect¶

An external operation a function performs, e.g. filesystem, database, network, system, state mutation, or time access. Functions must declare the external effects they perform and cannot perform undeclared effects.

Source: language-guide/permissions.md, technical-specification/TECHSPEC-09.md.

Permission¶

Explicit authorization to perform an effect. Permissions must be granted explicitly and follow least privilege; calling a function must not silently grant additional permissions.

Source: language-guide/permissions.md, technical-specification/TECHSPEC-09.md.

Module¶

A separately compilable unit with a declared public interface and declared dependencies. Internal details remain private by default.

Source: language-guide/modules.md, technical-specification/TECHSPEC-08.md.

Interface¶

A declaration of required functions, associated types, and behavioral requirements that a type promises to provide. Implementation must be explicit.

Source: technical-specification/TECHSPEC-41.md.

Trait¶

A reusable capability (e.g. equality, ordering, iteration) declared as operations and constraints. Trait implementation must be explicit.

Source: technical-specification/TECHSPEC-41.md.

Diagnostic¶

A structured compiler message. Every diagnostic must include a unique error identifier, category and severity, exact source location, description, violated rule or contract, expected vs. actual behaviour, and suggested investigation steps.

Source: compiler/diagnostics.md, technical-specification/TECHSPEC-12.md.