# `ExTLA.Spec`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/spec.ex#L1)

`use ExTLA.Spec` turns a module into a specification.

    defmodule Specs.Counter do
      use ExTLA.Spec

      constant :max
      variable :n, type: 0..^max

      init do
        n = 0
      end

      action :increment do
        require n < ^max
        n = n + 1
      end

      invariant :within_bounds do
        n >= 0 and n <= ^max
      end
    end

The declarations accumulate into module attributes and compile to ordinary
functions on the module; `@before_compile` assembles them into a
`ExTLA.Spec.Compiled` struct, reachable as `Specs.Counter.__tla_spec__/0` or
`ExTLA.Spec.Compiled.from_module/1`.

The DSL's semantics are normative in `02-dsl-semantics.md`, and every rule
there is enforced when this module compiles — a spec either means something
precise or does not compile.

---

*Consult [api-reference.md](api-reference.md) for complete listing*