FORMAL SPECIFICATION AND REFINEMENT FOR AN
INTERACTIVE WEB EXAMPLE
Ingrid van Coppenhagen
School of Computing, University of South Africa (Florida Campus), Private Bag X6, Florida, South Africa, 1710
Barry Dwolatzky
School of Electrical & Information Engineering, University of the Witwatersrand, Private Bag 3, Wits, South Africa, 2050
Keywords: Implementation, interactive, refinement, specification, Web, XML, Z.
Abstract: This paper provides a small interactive Web example (the Car1 example) that illustrates parts of the
software life cycle processes of specification, refinement and implementation in an object-oriented
environment. Part of the software system is specified in Z, data- and operation refined and then
implemented into HTML, XML, XSD and JavaScript. Short descriptions of the refinement processes
comprising data refinement, operation refinement and operation decomposition are given. The main focuses
of the study are to firstly investigate how effective (or not) a formal specification is for an interactive Web
system, and secondly to illustrate a selection control structure in the refinement process.
1 INTRODUCTION
This paper evaluates the specification of a part of a
small interactive Web system (the Car1 example) in
Z, the subsequent data and operation refinement, and
then the implementation into HTML, XML, XSD
and JavaScript.
One of the aims of the paper is to evaluate how
effective a formal specification is for the Car1
example, with particular emphasis on the use of a
selection control structure. This control structure has
been specified and refined formally and in detail.
In sections 2, 3, and 4 the concepts of
specification, refinement, and control structures are
described respectively. From Section 5 the Car1
example is presented, with the previous three
concepts included. In Section 9 some conclusions
are drawn. Following Section 9 are the references,
Appendix A which contains the programs of the
Car1 example and Appendix B which explains some
Z notation.
2 SPECIFICATION
The Z notation uses mathematical concepts,
particularly set theory, to specify data and
operations. This allows for reasoning about systems,
for example checking the consistency of the data and
the various operations, as well as verifying the
correctness of subsequent system development
during refinement (Ratcliff, 1994, Lightfoot, 2001,
Smith, 2000, Woodcock, 1996, Jacky, 1997).
3 REFINEMENT
The two main stages of refinement are data
refinement and operation refinement. Data and
operation refinement can be looked at as that part of
the development process that corresponds to the
design phase of the traditional software life cycle.
Ways to represent the abstract data structures that
will be more amenable to computer processing are
chosen, as well as the translation of abstract
operations into corresponding concrete operations.
The concrete operations are, however, still expressed
in the language of schemas (using Z) and describe
only the relationship among the components of
before and after stages. This does not indicate how
89
van Coppenhagen I. and Dwolatzky B. (2006).
FORMAL SPECIFICATION AND REFINEMENT FOR AN INTERACTIVE WEB EXAMPLE.
In Proceedings of WEBIST 2006 - Second International Conference on Web Information Systems and Technologies - Internet Technology / Web
Interface and Applications, pages 89-96
DOI: 10.5220/0001237100890096
Copyright
c
SciTePress
such changes of state are to be expressed in an
implementation computer language (Ratcliff, 1994,
Jacky, 1997, Derrick, 2001).
In operation refinement the process of
conversions of descriptions of state changes can be
carried into executable instruction sequences.
4 CONTROL STRUCTURES
All programs can be written in terms of only three
control structures, namely the sequence structure,
the selection structure and the repetition structure.
The if structure is called a single-selection structure,
because it selects or ignores a single action. The
if/else structure is called a double-selection
structure, because it selects between two different
actions (or groups of actions) (Deitel, 2002).
5 THE CAR1 EXAMPLE
In brief, in the Car1 example, the information of 6
cars is given in an XML document car1.xml. This
information is used to display the Web site
demonstrated in Figure 2. The make, model number,
year, price and picture of each car are given. The
price of some cars is more than R200000.00 and
some are less. The user can choose either one to get
a display of the make, model number, year and price
for the relevant cars. This if selection structure in the
JavaScript program constitutes the crux of the
discussion regarding the refinement of the
specifications of the programs.
6 Z SPECIFICATIONS
Basic types, sets, data, constants, choices and
messages: Basic types (given sets):
[MAKE, MODEL, YEAR, PRICE, IMAGE, X]
Refer to figures 1. The following are these sets:
X = {01, 02, 03, 04, 05, 06} e N This represents
the record counter for the data.
MAKE = {(01, Peugeot), (02, Audi), (03, Citroën),
(04, Mazda), (05, Mercedes), (06, Mercedes)} e X
ß MAKE
MODEL = {(01, 307CC), (02, A6), (03, C5), (04,
1.6), (05, E-class), (06, SLRMcLaren)} e X ß
MODEL
YEAR = {(01, 2004), (02, 2004), (03, 2004), (04,
2004), (05, 2002), (06, 2004)} e X ß YEAR
PRICE = {(01, 250000.00), (02, 340000.00), (03,
150000.00), (04, 170000.00), (05, 540000.00), (06,
640000.00)} e X ß PRICE
IMAGE = {(01, car(01).jpg), (02, car(02).jpg), (03,
car(03).jpg), (04, car(04).jpg), (05, car(05).jpg), (06,
car(06).jpg)} e X ß IMAGE
STR::= Price| Year| Model| Over| Under; N: Natural
numbers; : Empty set; maxSize: N; n: N The
number of cars. For this example n = 6.
Table 1: Car1 data file (given in car1.xml).
X
(recor
d
counte
r)
make model year img price
01 Peugeot 307CC 2004 car(01).jpg 2500
00.0
02 Audi A6 2004 car(02).jpg 3400
00.0
03 Citroën C5 2004 car(03).jpg 1500
00.0
04 Mazda 1.6 2004 car(04).jpg 1700
00.0
05 Mercedes E-class 2002 car(05).jpg 5400
00.0
06 Mercedes SLRMcLaren 2004 car(06).jpg 6400
00.0
»_Car_System
_________________
___
ƻ____________________
ÆÆcar1.html (User Interface)
ÆÆcar1.js; car1.xml; car1.xsd
Æ–____________________
–__________________________
Figure 1a: The Z Car system.
»_car1.html
__________________
___
ÆDisplay Welcome page; On click: car1.js [Detail of this
Æspecification not relevant to the discussion]
–__________________________
Figure 1b: The Car1.html file (User Interface).
»_car1.xml_____________________
Æx: P X [X is not a field in the record, it is used
Æonly in the schema as a record counter]
Æmake: Xß MAKE; model: Xß MODEL;
Æyear: Xß YEAR; img: Xß IMAGE;
Æprice: Xß PRICE; n: N; car1.xsd;
«_______________
Æ (x = dom make; dom model; dom year; dom
Æ img; dom price); n = 6
–__________________________
Figure 1c: car1.xml.
»_car1.xsd_____________________
Æ X car1.xml
Æ[Information not relevant to the discussion of this paper]
–__________________________
Figure 1d: car1.xsd.
WEBIST 2006 - INTERNET TECHNOLOGY
90
»__car1.js_____________________
Æ »__________________
Æ ÆX car1.html; X car1.xml; X car1.xsd
Æ Æmake!; model!; price!; img!; year!
Æ Æn: N; n = 6; str?: STR
Æ –____________________
Æ »_Init_________________
Æ Æx' = 0
Æ –____________________
Æ »_showPix()______________
Æ Æ(Ai:0..(n-1) make(i)!
model(i)! img(i)!)
Æ –____________________
Æ »_range(str)___________ ___
Æ Æ(str? = 'Over') (E i:0..(n-1) price(i) > 200000
Æ Æ¶ make(i)! model(i)! price(i)! year(i)!
Æ Æimg(i)!)
Æ Æ(str? = 'Under') (E i:0..(n-1)
price(i) < 200000
Æ Æ¶ make(i)! model(i)! price(i)! year(i)!
Æ Æimg(i)!)
Æ –____________________
Æ »_ListAll(str)______________
Æ Æ[Information not relevant to the discussion of this
Æ Æ paper]
Æ –____________________
–__________________________
Figure 1e: car1.js.
7 VERIFICATION AND
REFINEMENT (Z)
The Z data specifications for the schema Car1.xml
data types and operation specifications for the
schema range(str) can be refined as follows:
7.1 Verifying Consistency of Global
Definitions
For the axiomatic description
ÆGlobalDeclarations
«_____________
ÆGlobalPredicates
it must be established that there exists values for
GlobalDeclarations that satisfy GlobalPredicates.
For example from the type definitions, the state
variables can be defined as follows:
Æx: PX; make: X ß MAKE; model: X ß MODEL
«_______________________
Æ(x = dom make; dom model)
Figure 2: The Car Website.
FORMAL SPECIFICATION AND REFINEMENT FOR AN INTERACTIVE WEB EXAMPLE
91
Suppose x = {03} and make = {Citroën}.
Therefore x = dom make. Therefore Hx: PX
make: X ß MAKE true. By a simple property of
logic H true. Also
Æmake: MAKE (declaration of constant)
«______________
Æmake = Citoën (value of constant)
This description is consistent because it does not
contradict x's declaration.
A number of consistency checks can be
performed on the state space of Figure 1c.
Æx: X; make: MAKE
«______________
Æx = 03; make = Citroën
This axiomatic description is also a verification
of the consistency of the global definitions or H
Car1.xml' x'
X make' MAKE which for the
axiomatic description is true, therefore H
Car1.xml' true and by a simple property of logic
H true. This satisfies the verification for global
definitions, which can also serve as part of a data
refinement because a concrete data type was
constructed that simulates the abstract one.
7.2 Verifying Consistency of an
Initial State
A check must be done to ensure that a consistent
initial state exists. This check can be expressed as
the initialisation theorem which has the following
general form: H State' InitStateSchema which can
be extended to H State'; Inputs? InitStateSchema
if there are input variables for the initial state
schema InitStateSchema.
The concrete initial state for Car1.js is:
»_init _____________________
Æx' =
–________________________
To show that it is consistent:
H x': PX; make': X ß MAKE x' = dom make'.
If dom make' = then x' = which implies that
there is a state Car1.js' of the state definition schema
that satisfies the initial state description.
The above mentioned checks can also serve as
data refinement where it must be determined
whether every abstract state has at least one concrete
representative and there exists a consistent initial
state.
7.3 Verifying Consistency of
Operations
For an operation that is defined as:
OperationDeclarations | OperationPredicates, the
consistency theorem is H OperationDeclarations
OperationPredicates.
Calculating its precondition can check an
operation’s consistency. If the operation is
inconsistent, its precondition will be false. A false
precondition strongly suggests a defect in the
operation description (Ratcliff, 1994).
The consistency theorem for the operation
range(str) will be: (str? = ‘Over’) (E i:0..(n-1)
price(i) > 200000 make(i)! model(i)! price(i)!
year(i)! img(i)!).
Now assume that (str? = 'Over') false
then (Ei:0..(n-1) price(i) < 200000 make(i
)!
model(i)! price(i)! year(i)! img(i)!).
But according to the second statement in
range(str) (Figure 1e): if (str? =Under’) (E
i:0..(n-1) price(i) < 200000 make(i)! model(i)!
price(i)! year(i)! img(i)!).
Then according to a simple property of logic H
(str? =Over’) (E i:0..(n-1) price(i
) < 200000
make(i)! model(i)! price(i)! year(i)! img(i)!)
false and then according to a simple property of
logic H false. This means that the assumption was
false, and that the sequent predicate is not a
contradiction, hence that range(str) is consistent.
This means that the assumption was false, and
that the sequent predicate is not a contradiction,
hence that range(str) is consistent.
7.4 Data Refinement
Refer to Figure 1c, the abstract state Car1.xml,
with an initial state:
»_init_Car1.xml__________________
ÆCar1.xml'
«____________________
Æx' =
–_________________________
WEBIST 2006 - INTERNET TECHNOLOGY
92
and with (for example) an abstract operation on the
data being the operation schema range(str) (from
Figure 1e).
We plan to implement this system into a
programming language that supports arrays and lists.
We decide to refine the abstract specification to a
detailed design based on sequences because we
expect this will be easier to map into the target
programming language. The reason for this is
because sequences are sorted lists.
For the refinement the concrete representation of
Car1.xml is not a set but a sequence Car2.xml of
elements of type X, X ß MAKE, X ß MODEL, X
ß YEAR, X ß IMAGE and X ß PRICE.
The concrete representative x is not a set but a
sequence x1. The state set Car1.xml is re-expressed
as:
»_Car2.xml____________________
Æx1: seq X; make1: seq (X ß MAKE);
Æmodel1: seq (X ß MODEL); year1: seq (X ß YEAR);
Æimg1: seq (X ß IMAGE); price1: seq (X ß PRICE);
«____________________
Æ(# ran x1 = # ran make1; # ran model1; # ran year1; #
Æran img1; # ran price1)
–_________________________
Here is the concrete selection control structure
operation of range(str):
»_range1(str)____________________
Æ(str? = 'Over') (E i:0..(n-1) price1(i) > 200000
Æmake1(i)! mode1l(i)! price1(i)! year1(i)!
Æimg1(i)!)
Æ(str? = 'Under') (E i:0..(n-1) price1(i) < 200000
Æmake1(i)! mode1l(i)! price1(i)!
year1(i)!
Æimg1(i)!)
–__________________________
The sequence should always hold the same
elements as the set. A sequence is a function from
natural numbers to elements, so the elements stored
in the sequence are the range of this function. The
range of the sequence must be the same as the set.
x = ran x1 x' = ran x1' also price = ran price1
price' = ran price1', etc..therefore (E i:0..(n-1)
price(i) > 200000 (E i:0..(n-1) ran price1(i) >
200000).
This must be true before and after any operation,
so equations appear for unprimed and primed (')
variables. We now form the implication that
expresses the refinement. The predicate of the
abstract operation range(str) appears on the right of
the implication arrow, and the predicate of the
concrete operation range1(str) is on the left, along
with the equations relating make, make1, model,
model1, year, year1, img, img1, price and price1.
When (
str? = 'Over') then (E i:0..(n-1) price1(i)
> 200000) price = ran price1 price' = ran
price1'. Also when (str? = 'Under') then (E i:0..(n-
1) price1(i) < 200000) price = ran price1
price' = ran price1'
7.5 Proof of the Selection Control
Structure Refinement
When (str? = 'Over') then (Ei:0..(n-1) price1'(i)
> 200000) = (Ei:0..(n-1) price1(i) > 200000)
price = ran price1 price' = ran price1' price' =
price.
¤ (Ei:0..(n-1) price'(i) > 200000)
[Assume
antecedent]
¤ (Ei:0..(n-1) ran price1'(i) > 200000)
[Antecedent price' = ran price1']
¤ (Ei:0..(n-1) ran price1(i) > 200000) [Given]
¤ (Ei
:0..(n-1) price(i) > 200000)
[Antecedent price = ran
price1]
¤ true
An equivalent proof for when (str? = 'Under').
7.6 Verifying the Correctness of the
Concrete Initial State
The concrete initial state must not describe initial
states that have no counterpart in the abstract model
(Ratcliff, 1994, Jacky, 1997, Derrick, 2001). A
theorem of the following form is to be proved:
Given the retrieve relation then: InitConcState H
InitAbsState which says that ‘for each concrete
initial state, there is a corresponding abstract one’.
Refer to the following schema definitions:
»_init_Car1.xml___________________
ÆCar1.xml'
«____________________
Æx' =
–__________________________
and from the Data refinement the Car2.xml schema
and
FORMAL SPECIFICATION AND REFINEMENT FOR AN INTERACTIVE WEB EXAMPLE
93
»_Car2.xml'_____________________
Æx1': seq X; make1': seq (X ß MAKE);
Æmodel1' : seq (X ß MODEL); year1': seq (X ß YEAR);
Æimg1': seq (X ß IMAGE); price1': seq (X ß PRICE);
«____________________
Æ(# ran x1' = # ran make1'; # ran model1'; # ran year1';
Æ# ran img1'; # ran price1')
–__________________________
and
»_init_ Car2.xml_________________
ÆCar2.xml'
«____________________
Æx1' = 〈〉
–_________________________
and from the Data refinement the Car1.xml schema
and
»_CARel_____________________
ÆCar1.xml; Car2.xml
«____________________
Æx = ran x1
–_________________________
and
»_CARel'
_
____________________
ÆCar1.xml'; Car2.xml'
«____________________
Æx' = ran x1'
–_________________________
It must be proved that there is a state CARel' of
the general model CARel (concrete to abstract
relation) that satisfies the following: init_ Car1.xml H
init_ Car2.xml.
CARel' acts as an extra hypotheses (given
CARel'). The declarative part of the right-hand side
schema text is just Car1.xml' which is provided by
CARel' on the left. The sequent is then unfolded into
CARel'; Car2.xml' x1' = 〈〉 H x' = which holds
because x1' = 〈〉 on the left and x' = ran x1' in
CARel'.
By substitution x' = ran 〈〉, and x' =
immediately follows.
7.7 The concrete State Must be
Consistent
It has to be shown in general that
H ConcState' InitConcState (InitConcState
represents the initial concrete state) or for our
example: H Car3.xml' init_Car2.xml
Car3.xml' is a state of the general model Car3.xml.
From the Data refinement it is concluded that the
state sets x: PX; make: X ß MAKE; model: X ß
MODEL; year: X ß YEAR; img: X ß IMAGE;
price: X ß PRICE; are implemented as arrays with
an index variable: x1: array [0..(maxSize-1)];
make1: array[0..(maxSize-1)]; model1: array
[0..(maxSize-1)]; year1: array[0..(maxSize -1)];
img1: array[0..(maxSize-1)]; price1:
array[0..(maxSize-1)]; n: 0..(maxSize-1).
It is assumed that the n elements of the x1 array
are sorted in ascending sequence to ensure that no
duplicates are kept in the array and to facilitate fast
lookup of the array. For all the n elements of the x1
array, the corresponding elements in the make1,
model1, year1, img1, and price1 arrays have the
same element number as the number of the x1 array.
For example, make1(3) is the car make of the car
represented by x1(3).
Add the following to Car1.xml: maxSize: N to
give:
»_car3.xml_____________________
Æx: P X; make: Xß MAKE; model: Xß MODEL;
Æyear: Xß YEAR; img: Xß IMAGE;
Æprice: Xß PRICE; n: N; car1.xsd
«_______________
Æ(x = dom make; dom model; dom year; dom img; dom
Æprice); #x¯ maxSize -1; n = 6
–__________________________
»_Car4.xml_____________________
Æx1: seq X; make1: seq (X ß MAKE)
Æmodel1 : seq (X ß MODEL); year1: seq (X ß YEAR);
Æimg1: seq (X ß IMAGE); price1: seq (X ß PRICE);
Æn = 0..(maxSize -1)
«____________________
Æ(# ran x1 = # ran make1; # ran model1; # ran year1;
Æ#ran img1; # ran price1); #x1 = n
ÆAi,j: dom x1 i < j x1(i) < x1(j); n' = n
–__________________________
»_Car4.xml'_____________________
Æ
x1': seq X; make1': seq (X ß MAKE);
Æmodel1' : seq (X ß MODEL); year1': seq (X ß YEAR);
Æimg1': seq (X ß IMAGE); price1': seq (X ß PRICE);
Æn = 0..(maxSize -1)
«____________________
Æ(# ran x1' = # ran make1'; # ran model1'; # ran year1';
Æ# ran img1'; # ran price1'); #x1' = n''
ÆAi,j: dom x1' i < j x1'(i) < x1'(j); n' = n
–__________________________
To show that it is consistent: Refer to Car4.xml':
H x1': seq X; n': 0..(maxSize-1); i, j: dom x1' i <
j x1'(0) < x1'(1) < x1'(2), < .. x1'(maxSize-1);
WEBIST 2006 - INTERNET TECHNOLOGY
94
#x1' = n'. If n' = 0 then x1' = 〈〉 that implies that there
is a state (Car4.xml') of the general model Car4.xml
that satisfies the initial state description init_
Car2.xml.
7.8 Determine Whether Every
Abstract State Has at Least One
Concrete Representative
This can be achieved by determining if each abstract
variable can be derived or ‘retrieved’ from the
concrete variables by writing down equalities of the
form: AbsVar = Expr(ConcVars) where AbsVar
represents an abstract variable of the abstract state,
Expr an expression and ConcVars the concrete
variable of the concrete state representing the
abstract state.
For the example the predicate x = ran x1 will be
referred to as the ‘retrieve relation’ CARel (concrete-
to-abstract relation) that brings together the abstract
and the concrete states:
»_CARel____________________
ÆCar1.xml; Car2.xml
«____________________
Æx = ran x1
–________________________
The equality means that CARel is in effect a total
function when viewed as ‘calculating’ the abstract
state from the concrete one. Being total means that
every concrete state maps to some abstract state.
This implicit property of the retrieve relation being
functional and total, characterises the fact that a
simplified form of data refinement is discussed
(Ratcliff, 1994).
Suppose, however, the ‘sorted’ invariant was
removed from Car2.xml so that the array element
order was immaterial. Assume that no duplicates are
stored in the array. The design will now include
some redundancy in that each non-empty, non-
singleton set in the abstract state would have more
than one concrete representation (Ratcliff, 1994).
For example, the abstract state
model {307CC, A6, C5, 1.6, E-class,
SLRMcLaren} will have 6! concrete representatives
(of which two are shown): model1 1.6,
307CC,.., C5, n 6 and model1 C5,
1.6,..A6, n 6
In general, assuming no duplicates, there would
be n! concrete representatives for a single abstract
state. The implicit functionality of a retrieve relation
such as CARel is not compromised because the
relation expresses a calculation from concrete to
abstract (Ratcliff, 1994).
7.9 Operation Refinement
Refer to range1(str) from the Data refinement with
n' and n added:
»_range1(str)____________________
Ærange1(str)
Æn' = n
–__________________________
This is a data-refined operation because the
abstract range(str) operation is re-expressed as the
concrete operation range1(str). range1(str) is
refined into range2(str):
»_range2(str)____________________
Æ(str? = 'Over') ((E i:0..(n-1) price1(i) > 200000)
Æ(θCar4.xml' = θCar4.xml) ((i)@ make1)! ((i)@
Æmodel1)! ((i)@ price1)! ((i)@ year1)! ((i)@ img1)!)
Æ(str? = 'Under') ((E i:0..(n-1)
price1(i) < 200000)
Æ(θCar4.xml' = θCar4.xml) ((i)@ make1)!
Æ((i)@ model1)! ((i)@ price1)! ((i)@ year1)! ((i)@
Æ img1)!)
Æ n' = n
–_________________________
((i) @ make1) extracts the ith element of array make1.
range2(str) can be refined into the following
algorithm: (Let n be the number of Cars).
[lookFor(str?, range(str))]
[Send str to the function range(str) (in car1.js)]
for i = 0..(n-1)
if str = 'Over' and price(i) > 200000.00
[Check for car prices > 200000]
display make(i), model(i), year(i), img(i), price(i);
[Display the values on the
website]
else
if str = 'Under' and price(i) < 200000.00
[Check for car prices < 200000]
display make(i), model(i), year(i), img(i), price(i);
[Display the values on the
website]
endif
endif
endFor
This algorithm is implemented by the range(str)
function of the car1.js program (refer to Appendix
A).
FORMAL SPECIFICATION AND REFINEMENT FOR AN INTERACTIVE WEB EXAMPLE
95
8 IMPLEMENTATION
The programs are provided in Appendix A. The
programs include a car1.html program that provides
the user interface, the car1.xml and its corresponding
schema program car1.xsd provide the data input, and
car1.js is a javascript program that does the
calculations. This aids in the understanding of the
process of refinement if the end product (the
programs) are given to indicate where the algorithms
of the refinement are leading to. The output of the
programs should correspond with the results of the
data refinements and the instantiations. This serves a
dual purpose in that the output can be verified
against the instantiations, and the instantiations
against the output. Therefore the implementation
serves to verify that the specifications are correct,
and the specifications serve to verify that the
implementation is correct (Dong, 2004, Sun, 2002,
Woodcock, 1996, Deitel, 2002, Doke, 2002,
McGrath, 2002).
9 CONCLUSION
From the extensive refinement of the selection
control structure used on the data file, it can be
concluded that such a detailed specification and
refinement as illustrated in this paper will definitely
reduce errors in the coding of the programs. The
application of formal specifications and refinements
also serves a dual purpose in that the code can be
verified against the specifications, and the
specifications can be verified against the code.
REFERENCES
Ratcliff, B., 1994. Introducing Specification using Z.
McGraw-Hill Book Company.
Dong, J.S., 2004. Semantic Web and Formal
Specifications. Short version of ICSE'04 tutorial.
Computer Science Department, National University of
Singapore.
Sun, J., Song Dong, J., Liu, J., Wang, H., 2002. A Formal
Approach to the Design of ZML. Annals of Software
Engineering 13, 329-356.
Lightfoot, D., 2001. Formal Specifications using Z.
Palgrave.
Smith, G., 2000. The Object-Z specification language.
Kluwer Academic Publishers.
Woodcock, J., and Davies, J., 1996. Using Z Specification,
Refinement and Proof. Prentice Hall.
Deitel, H. M., Deitel, P. J., and Nieto, T. R., 2002. Internet
& World Wide Web How to Program. Prentice Hall.
Jacky, J., 1997. The Way of Z. Cambridge University
Press.
Derrick, J., and Borten, E., 2001. Refinement in Z and Z.
Foundations and Advanced Applications, Springer-
Verlag London.
Doke, E., Satzinger, J. W., and Williams, S. Rebstock,
2002. Object-Oriented Application using Java. Course
Technology, Thomson Learning.
McGrath, M., 2002. XML in easy steps. Computer Step.
APPENDIX A
http://www.unisa.ac.za/contents/colleges/col_science_eng
_tech/docs/ingrid/AppendixA.doc
APPENDIX B
Z NOTATION
http://www.unisa.ac.za/contents/colleges/col_science_eng
_tech/docs/ingrid/AppendixB.doc
WEBIST 2006 - INTERNET TECHNOLOGY
96