Z Notation
The Z Notation is a formal specification language used for describing and modeling programs.
Schemas
A schema consists of two parts: a declaration of variables, and a predicate constraining their values
[ seating : ℙ Seat; sold : Seat ⇸ Customer | dom sold ⊆ seating ]
The schema type of a schema simply removes all predicates.
Schema Operations
The theory of schema operations is, to put it politely, fucked. All operations are sensitive to the names being used, which makes schema operations no longer stable under Alpha Equivalence.
[ a : A, b : B | P ] ∧ [ b : B, c : C | Q ] ↦ [ a : A, b : B, c : C | P ∧ Q ]
Moreover, you have some batch name operations: if you have a schema
State := [ a : A, b : B | P ]
Then State' is the schema
State' := [ a' : A, b' : B | P[a'/a, b'/b] ]
You can also quantify over schemas, which shifts variables into the predicate. Finally schema composition is the most bizzare of all: it is a combination of Composition of Relations and a bulk rename.