Kifejezések
Alaptípus definiciók
Egy alaptípus definíciója egy vagy több alaptípust vezet be.A nevük nem lehettek korábban globálisan deklarálva és a hatókörük a definíciótól a specifikáció végéig tart.A nevük az alaptípusok globális szótárának része lesz.
Példa:
[NAME,DATE]
Axiómatikus leírások
Az ilyen leírás egy vagy több globális változót vezet be és opcionálisan meghatároz rajtuk egy megszorítást. A változók nem lehettek korábban globálisan deklarálva és a hatókörük a deklarációtól a specifikáció végéig tart.
Példa:
square : ℕ->ℕ
∀ n : ℕ square(n)= n * n
Megszorítások
???
Példa:
n_db < 5
Séma definíciók
Először bevezetjük a séma nevét.Ez lesz összeasszociálva az általunk felsorolt deklarációkkal és predikátumokkal.Előtte nem lehetett ugyanilyen nevű sémánk és a séma neve a specifikáció végéig megmarad.Ha predikátumot nem definiálunk akkor általánosan true értéket vesz fel.A séma jobb oldala a séma kifejezés amit segítségével akár régi sémákat is kombinálhatunk a séma kalkulus segítségével.
Példa:
BirthdayBook≙[known: ℙ NAME;...]