Mathematical set theory has the notion of a type - for example
integers, booleans.
Z allows another type, the schema type. A schema consists of
two parts divided by a horizontal line. In the upper half we have what is
commonly referred to as the <#1119#> declarative<#1119#> part of the schema. Here we
define our variables by stating their type. In the second half, or bottom
half, commonly referred to as the <#1120#> predicate<#1120#> part, we show how the
variables are constrained.
<#1121#>SCHEMA-NAME<#1121#>
declarations
predicates
by+
Modularity and abstraction are important assets of Z, and this is coped
with by allowing schemas to be written in the declarative part of other
schemas.
<#1122#>SCHEMA2<#1122#>
SCHEMA1
more
\
declarations
more
\
predicates
by+
And this should be read by imaging the schema <#1123#> Schema1<#1123#> expanded, with
all of its declarations joining the <#1124#> more declarations<#1124#> of <#1125#> Schema2<#1125#>
and all its predicates being moved under the dividing line to join the <#1126#>
more predicates<#1126#> of <#1127#> Schema2<#1127#>
The way operations are described in Z, for a given schema, is to relate the
variables of the state after the operation (dashed) to the variables of the
state before the operation (undashed).
So for an operation <#1128#> OP<#1128#> on a schema <#1129#> Schema1<#1129#> we would have
<#1130#>OP<#1130#>
SCHEMA1
SCHEMA1'
Show
\
how
\
the
\
variables
\
of
\
the
\
before
\
and
\
after
\
state
\
are
\
related.
by+
This is notion of change is made explicit by the delta schema, which expresses
the fact that some state has changed in a schema, without the need to repeat
the entire definition
<#1131#> SCHEMA1<#1131#>
SCHEMA1
SCHEMA1'
by+
So a delta schema says we have some previous state, and some next state, and
that the state has changed. The converse of this, is where an operation
produces no change-
<#1132#>OP<#1132#>
SCHEMA1
SCHEMA1'
All
\
the
\
variables
\
of
\
the
\
before
\
and
\
after
\
state
\
are
\
unchanged
by+
This is written: ` #tex2html_wrap_inline4176#'
Other notation is best described by example. Consider the following schema
<#1133#>EXAMPLE<#1133#>
a,b :
x,y :
p,q :
(
)
f,g :
seq1,seq2 :
[Names]
name :
Names
a ;SPM_gt; b
z :
\
|
\
z ;SPM_gt; a
z ;SPM_lt; fst
\
x
n : (
)
\
|
\
n
p
fst
\
n
=
\
snd
\
n
q =
{
s,t :
\
|
\
s ;SPM_gt; t
t ;SPM_lt; s
(s,t)
}
n :
f
\
n =
{ m :
\
|
\
m ;SPM_lt; n
m
}
g =
{
1,2,3
}
f
seq1 = [mary, sally, john]
seq2 =
{
1
}
seq1
name =
seq2
by+
In the declarative part of the schema we declare our variables.
- <#1135#> a<#1135#> and <#1136#> b<#1136#> are natural numbers.
- <#1137#> x<#1137#> and <#1138#> y<#1138#> are pairs of natural numbers.
- <#1139#> p<#1139#> and <#1140#> q<#1140#> are some subset of natural numbers.
- <#1141#> f<#1141#> and <#1142#> g<#1142#> are functions which take a number and return some
subset of numbers.
- <#1143#> seq1<#1143#> and <#1144#> seq2<#1144#> are sequences of names, in Z, this sequence
is thought of as a function from the natural numbers to the set of names.
- The variable <#1145#> name<#1145#> is a subset of names.
We consider the predicate part of the schema, one line at a time.
- <#1148#> a<#1148#> is bigger than <#1149#> b<#1149#>
- there exists a number which is bigger than <#1150#> a<#1150#>, but smaller than
the first element of the pair <#1151#> x<#1151#>
- any pair of numbers contained in the subset of pairs of
numbers <#1152#> p<#1152#>, must have equal values, e.g like (3,3)
- the set <#1153#> q<#1153#> is constructed by pairs of numbers, which satisfy the
condition of neither is greater than the other (hat is they are the same),
so <#1154#> p<#1154#> and <#1155#> q<#1155#> have a similar structure
- <#1156#> f<#1156#> is the function, which takes a number and returns the set of
numbers which has all the numbers up to but not including that number
- g is the function which is like <#1157#> f<#1157#>, but only defined for the
values 1,2 and 3. This is known as <#1158#> domain restriction<#1158#>
- gives an explicit value for <#1159#> seq1<#1159#> is, which, in Z, is equivalent
to the function
#tex2html_wrap_inline4178#
- Tells that <#1160#> seq2<#1160#> is like <#1161#> seq1<#1161#> only restricted to the first
element, i.e. <#1162#> seq2 = [mary]<#1162#>, or equivalently #tex2html_wrap_inline4180#
- Says that the variable <#1163#> name<#1163#> has the value which is given by the
range of <#1164#> seq2<#1164#>, more specifically #tex2html_wrap_inline4182#
One more thing, writing <#1166#> EXAMPLE.f<#1166#>, for example, refers to the variable
<#1167#> f<#1167#> as defined in the schema <#1168#> EXAMPLE<#1168#>.