Regarding the Z Specification

[Steven Nieh]

Hello Everyone, I have a general question for Z Specification. In the
systemState, do we usually need a set to store the current information we
need? For example, in the 2003 final, we use the reuqest set(Please refer
to the solution) to record the toys we need to make all the time. Then, when we have a new
task, then we can simply "add" a new element in the record set; However,
in the 2005 final, we simply use the function RR to maintain the students
that live in the residence. Shouldn't we create a set to do it like the
one in 2003 final?

Also, in the AddStudent state, should we use delta ResidenceRoomDatabase
instead of deltaRR?

Thanks!

Steve

[Nancy Day]

Post by Steven Nieh
Hello Everyone, I have a general question for Z Specification. In the
systemState, do we usually need a set to store the current information
we need? For example, in the 2003 final, we use the reuqest set(Please
refer to the solution) to record the toys we need to make all the time.
Then, when we have a new task, then we can simply "add" a new element in
the record set; However, in the 2005 final, we simply use the function
RR to maintain the students that live in the residence. Shouldn't we
create a set to do it like the one in 2003 final?

I don't think I follow your question. In the 2005 final, the function RR
changes over time (see the last line of the AddStudent schema). In the 2003
final, the "requests" set stores different information than the "job"
function. Elves might make toys that have not been requested. It would
be a different operation to add a toy that an elf makes.

Post by Steven Nieh
Also, in the AddStudent state, should we use delta ResidenceRoomDatabase
instead of deltaRR?

You are correct. This is an error in the solution set.

cheers, nancy
--------------------------------------------------------------------
Nancy Day, Associate Professor
CS245 Winter 2009 Instructor
http://www.student.cs.uwaterloo.ca/~cs245
David R. Cheriton School of Computer Science, University of Waterloo