Section.
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.
where
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
and
∀ sym : String, sym in body-of (p (p sect - 1)) … bound? sym.
where
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).
where
env p : Program ⇒ [Scope].
base-env ⇒ Scope.
Scope = {String}.
