Pantagruel: An Extremely Lightweight Specification Language

Program = [Section].
eval p : Program ⇒ Bool.

A section head must have at least one statement; a section body can be empty.

section head : Head, body : Body, #head > 0 ⇒ Section.
Head = [Comment + Declaration + Alias].
Body = [Comment + Expression].
(Comment, Declaration, Alias, Expression) = String.

eval p ↔ ∀ sect : Section, sect in p … all-bound? sect.


all-bound? sect : Section ⇒ Bool.

All variables referred to in a section head must be defined by the end of that section head. All the variables in a section body, however, must be defined by the end of the next section body.

all-bound? sect ↔
 ∀ sym : String, sym in head-of sect … bound? sym
 ∀ sym : String, sym in body-of (p (p sect - 1)) … bound? sym.


head-of sect : Section ⇒ Head.
body-of sect : Section ⇒ Body.
bound? sym : String ⇒ Bool.

bound? sym ↔ (sym in (env p) (p sect)) or (sym in base-env).


env p : Program ⇒ [Scope].
base-env ⇒ Scope.
Scope = {String}.


Learn More

Pantagruel on GitHub

Pantagruel Language Reference

A Specification of a Note-Taking Program