# Glossary

#### Auxiliary Code

Additional library code that is not written in the Wuffs programming language.
See the [auxiliary code](/doc/note/auxiliary-code.md) note for more details.

#### Axiom

A named rule for asserting new facts. See the
[assertions](/doc/note/assertions.md#axioms) note for more details.

#### Assertion

A compile-time directive that introduces a new fact (or fails to compile, if
the assertion cannot be proved). See the [assertions](/doc/note/assertions.md)
note for more details.

#### Call Sequence

An API restriction that e.g. the `foo` method needs to be called before the
`bar` method. Out of order calls may result in a `"#bad call sequence"` error.

#### Coroutine

A function that can suspend execution and, when called again later, resume
where it left off, in the middle of the function body. See the
[coroutines](/doc/note/coroutines.md) note for more details.

#### Dependent Type

A type that depends on another value. For example, a variable `n`'s type might
be "the length of `s`", for some other
[slice](/doc/note/slices-arrays-and-tables.md)-typed variable `s`. Dependent
types are *a* way to implement compile-time [bounds
checking](/doc/note/bounds-checking.md), but they're not the only way, and
there's more to programming languages than their type systems. Wuffs does not
use dependent types.

#### Effect

An extension of the type system, such as purity (freedom from side effects),
applied to functions. See the [effects](/doc/note/effects.md) note for more
details.

Syntactically, effects are the exclamation and question marks, `!` and `?`, at
function definitions and function calls. These denote impure and
[coroutine](/doc/note/coroutines.md) functions.

#### Fact

A boolean expression (e.g. `x > y`) that is guaranteed to be true at a given
point in a program. See the [facts](/doc/note/facts.md) note for more details.

#### Flick

A unit of time. One [flick](https://github.com/OculusVR/Flicks) (frame-tick) is
`1 / 705_600_000` of a second.

#### Hermetic Function

A function that can modify only local state (to store the result of
computation), not global or system state. See the
[hermeticity](/doc/note/hermeticity.md) note for more details.

#### Interval Arithmetic

Arithmetic on numerical ranges. See the [interval
arithmetic](/doc/note/interval-arithmetic.md) note for more details.

#### Method

A function whose first argument (the receiver) has special syntactic support.
For example, an expression like `foo.bar(etc)` might effectively be a function
call whose first argument is `foo` and whose remaining arguments are the `etc`.
It is syntactic sugar for `type_of_foo__bar(self: foo, etc)`. On the callee
(not the caller) side, that implicit argument is often named `self` or `this`,
depending on the language (e.g. Wuffs per se uses `this`, but Wuffs transpiled
to C uses `self` to avoid confusion with C++'s `this`). Wuffs has no free
standing functions, only methods.

#### Modular Arithmetic

Arithmetic that wraps around at a certain modulus, such as `256` for the
`base.u8` type. For example, if `x` is a `base.u8` with value `200`, then `(x +
70)` has value `270` and would overflow, but `(x ~mod+ 70)` has value `14`.

#### Operator Precedence

A ranking of arithmetic operators so that an expression like `a + b * c` is
unambiguous (for the computer), equivalent to exactly one of `(a + b) * c` or,
more conventionally, `a + (b * c)`. While good for brevity, Wuffs does not have
operator precedence: the bare `a + b * c` is an invalid Wuffs expression and
the parentheses must be explicit. The ambiguity (for the human) can be a source
of bugs in other [security-conscious file format
parsers](https://github.com/jbangert/nail/issues/7).

Some binary operators (`+`, `*`, `&`, `|`, `^`, `and`, `or`) are also
associative: `(a + b) + c` and `a + (b + c)` are equivalent, and can be written
in Wuffs as `a + b + c`.

#### Refinement Type

A basic type further constrained to a subset of its natural
[range](/doc/note/ranges-and-rects.md). For example, if `x` has type `base.u8[0
..= 99]` then it is an unsigned 8-bit integer whose value must be less than
`100`. Without the refinement, `x` could be as high as `255`.

Bounds may be omitted, where the base integer type provides the implicit bound.
`base.u8[0 ..= 99]` and `base.u8[..= 99]` are the same type.

`base.u8[0 ..= 99]` and `base.u32[0 ..= 99]` are two different types, as they
have different unrefined types. They can have different run-time
representations.

Non-nullable pointer types can be thought of as a refinement of regular pointer
types, where the refined range excludes the `nullptr` value.

#### Saturating Arithmetic

Arithmetic that stops at certain bounds, such as `0` and `255` for the
`base.u8` type. For example, if `x` is a `base.u8` with value `200`, then `(x +
70)` has value `270` and would overflow, but `(x ~sat+ 70)` has value `255`.

#### Situation

The set of [facts](/doc/note/facts.md) at a given point in a program.

#### Unsafe

A programming language mechanism (e.g. an `unsafe` keyword or package) to
circumvent the language's safety enforcement, typically used for performance or
very low level programming. Unlike some other memory-safe languages, Wuffs
doesn't have such an 'escape hatch'.

#### Utility Type

An empty struct (with no fields) used as a placeholder. Every written-in-Wuffs
function is a method: the receiver is mandatory. A Wuffs utility type's methods
are to its package what C++ or Java's static methods are to its class.

"Utility type" is merely a Wuffs naming convention. For example, Wuffs' `base`
package has a type called `base.utility`, similar to how the `zlib` package has
a type called `zlib.decoder`. Unlike "dependent type" or "refinement type",
"utility type" is not a phrase used in programming language type theory.

#### Work Buffer

Scratch space in addition to the primary destination buffer. For example, in
image decoding, the primary destination buffer holds the decoded pixels, but
while decoding is in progress, a decoder might want to store additonal state
per image column.

Wuffs' codecs can state the (input dependent) size of their work buffer needs
as a range, not just a single value. Callers then have the option to trade off
memory for performance.