Pantagruel: An Extremely Lightweight Specification Language

Thought.
Specification = [String].

Pantagruel is a language for writing system specifications.

pantagruel thoughts: [Thought] ⇒ Specification.

---

It’s a computer language, but not as you might think of it.

The effects of evaluating a specification are nil—Pantagruel has no execution semantics.

eval spec = null.

---

eval spec: Specification.
check spec: Specification ⇒ Bool.

---

However, Pantagruel specifications can be checked to ensure that certain conditions have been met.

For instance, that you’ve defined all your terms by the end of your document.

(∀ s <: invoked-symbols spec ⇒
 first-invoked-in-head? s spec → bound-as-of? s (first-appearance s spec)
 and
 first-invoked-in-body? s spec → bound-as-of? s (next-chapter (first-appearance s spec))) → check spec.

---

(Head, Body) = [String].
Chapter = (Head, Body).
Specification = [Chapter].

This allows a structured form of description where terms can be explained in gradually greater detail.

first-invoked-in-head? symbol: String, spec: Specification ⇒ Bool.
first-invoked-in-body? symbol: String, spec: Specification ⇒ Bool.

invoked-symbols spec: Specification ⇒ {String}.
first-appearance symbol: String, spec: Specification ⇒ Nat.

bound-as-of? symbol: String, position: Nat ⇒ Bool.
next-chapter n: Nat ⇒ Nat.

---

invoked-symbols spec =
 [∀ chapter <: spec, head-s <: (chapter 0) ⇒ head-s] +
 [∀ chapter <: spec, body-s <: (chapter 1) ⇒ body-s].

---

Expression.

Specifications can also be type-checked to ensure that your logic is consistent.

type-checks? expr: Expression ⇒ Bool.

---

(∀ expr <: expressions spec ⇒ type-checks? expr) → check spec.

---

expressions spec: Specification ⇒ [Expression].

---