Introduction to the Specification Language Z

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.
  1. <#1135#> a<#1135#> and <#1136#> b<#1136#> are natural numbers.
  2. <#1137#> x<#1137#> and <#1138#> y<#1138#> are pairs of natural numbers.
  3. <#1139#> p<#1139#> and <#1140#> q<#1140#> are some subset of natural numbers.
  4. <#1141#> f<#1141#> and <#1142#> g<#1142#> are functions which take a number and return some subset of numbers.
  5. <#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.
  6. The variable <#1145#> name<#1145#> is a subset of names.
We consider the predicate part of the schema, one line at a time.
  1. <#1148#> a<#1148#> is bigger than <#1149#> b<#1149#>
  2. there exists a number which is bigger than <#1150#> a<#1150#>, but smaller than the first element of the pair <#1151#> x<#1151#>
  3. any pair of numbers contained in the subset of pairs of numbers <#1152#> p<#1152#>, must have equal values, e.g like (3,3)
  4. 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
  5. <#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
  6. 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#>
  7. gives an explicit value for <#1159#> seq1<#1159#> is, which, in Z, is equivalent to the function #tex2html_wrap_inline4178#
  8. 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#
  9. 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#>.