### SCHEMA TYPES AND BINDINGS

Based on chapter 13 in The Way of Z.

Links to more Z lectures.

This page looks best when this and this X are about the same size: X. See these viewing tips.

A schema defines a new type whose instances are record-like objects called bindings.

There are only four kinds of data types in Z.

Basic types, [X], instances are individuals.

Set types, X, instances are sets.

Cartesian product types, X Y, instances are tuples.

Schema types, x: X; y: Y , instances are bindings.

Schema types and bindings enable Z to model large systems and support an object-oriented style.

CARTESIAN PRODUCT TYPES

Declare the Cartesian product type DATE.

 DATE == DAY MONTH YEAR

Instances of DATE are tuples.

 landing, opening: DATE landing = (20, 7, 1969) opening = (9, 11, 1989)

But nothing prevents tuples that indicate impossible dates.

 d: DATE d = (29, 2, 1997)

Cartesian product types cannot express constraints between components.

SCHEMA TYPES

Can express contraints between components.

 days == 31, 28, 31, 30, 31, 30, ..., 30, 31

 TypicalDate day: 1 .. 31 month: 1 .. 12 year: day days month

 (leap _) == {  y: 4*y  } \ ({  y: 100*y  } \ {  y: 400*y  })

 Feb29 month, day, year: month = 2 day = 29 leap year

 Date TypicalDate Feb29

SCHEMA TYPE SIGNATURE

The schema type is determined by the signature: names and types (but not the order) of state variables.

 TypicalDate day: 1 .. 31 month: 1 .. 12 year: day days month

The signature is visible after normalizing.

 TypicalDate day, month,year: day 1 .. 31 month 1 .. 12 day days month

The schema type is day, month, year: .

USING SCHEMA TYPES

Schema references can appear in declarations. The selector dot indicates particular state variables.

 landing: Date landing.day = 20 landing.month = 7 landing.year = 1969

or

 MultiEditor active: NAME buffer: NAME Editor active dom buffer

Schema references can be used as set valued expressions.

SCHEMA TYPE NOTATION

According to The Z Notation: A Reference Manual (ZRM), the notation for schema types and bindings is not part of Z itself.

This is not Z, according to the ZRM.

 landing: day, month, year: landing = day :> 20, month :> 7, year :> 1969

This alternative must be used instead.

 landing: Date landing.day = 20 landing.month = 7 landing.year = 1969

BINDING FORMATION OPERATOR,

S (theta S) is the (nameless) instance of schema type S which is in scope. Instead of

 weekday: Date 0 .. 6 d: Date weekday(d) = (d.day + ...) mod 7

we can write

 weekday: Date 0 .. 6 Date weekday( Date) = (day + ...) mod 7

Instead of

 Editor Editor left' = left right' = right

we can write

 Editor [  Editor | Editor' = Editor ]

SCHEMAS AS RELATIONS

We can use to define the binary relation corresponding to an operation schema.

 Precedes Date (year < year') (year = year' month < month') (year = year' month = month' day < day')

 precedes == {  Precedes ( Date, Date')  }

Now precedes is a binary relation on Date.

 Biography name: NAME birth, death: Date ... birth precedes death ...

Back to Z lectures.

Jonathan Jacky / University of Washington / Seattle, Washington / USA
E-mail: jon@u.washington.edu