Skip to main content

Logical DB Schemas

Rules specified in the logical schema must be true at every point in time, i.e. in each DB state.

Local Constraints​

x = V.x  
  
Email = String & Contains['@']  
# every customer must have a valid email address  
for_all[x: ET.Customer][x | F.email | is_a[Email]]  
  
# every customer must have a first name field set  
for_all[x: ET.Customer][x.first_name != nil]

The structure of Schema Constraints​

A typical constraint is formulated in the following form:
for_all[quantifier][sentence]

  • Quantifier: The quantifier specifies which values the variable can take on. Using an entity type and additional constraints is the typical pattern here.
  • Sentence: this is a clause which must evaluate to true for any valid database state (time slice). It can contain a combination of
    • variables
    • concrete instances (values or references to atoms)
    • ZefOps (and Zef Functions)

Non-Local Constraints​

# for a transaction to close: an account's balance may not be lower than its credit limit  
for_all[x: ET.Account][x.balance >= -x.credit_limit]  
  
  
# every minor must specify a guardian  
for_all[x: ET.Person & (Z.age<18)][x.guardian | is_a[ET.Person & (Z.age >= 18)]]
  • Zef DB schemas are in line with the