class registration system invariant

[Nancy Day]

In the class registration system (Wed's lecture), there
was an invariant to ensure the people could be on the
waiting list only if the class is full. It should be
written as:

(#enrolled < ClassLimit) <=> (waiting = <>)

cheers, nancy
CS245 Winter 2009 Instructor

[Donglin Han]

But what about the backward of IFF?
in the case of waiting = <>, it doesn't necessarily mean #enrolled <
ClassLimit. #enrolled could equal to ClassLimit, couldn't it?

Post by Nancy Day
In the class registration system (Wed's lecture), there
was an invariant to ensure the people could be on the
waiting list only if the class is full. It should be
(#enrolled < ClassLimit) <=> (waiting = <>)
cheers, nancy
CS245 Winter 2009 Instructor

[Nancy Day]

You're right. When the class limit has been reached, the waiting list might
have people on it or not. To be as precise as possible, could say:

(#enrolled < ClassLimit) => (waiting = <>)
(waiting = <>) => (#enrolled <= ClassLimit)

Or more concisely:

(waiting = <>) \/ (#enrolled = ClassLimit)

Because #enrolled cannot be greater than ClassLimit from another
invariant.

cheers, nancy

Post by Donglin Han
But what about the backward of IFF?
in the case of waiting = <>, it doesn't necessarily mean #enrolled <
ClassLimit. #enrolled could equal to ClassLimit, couldn't it?

Post by Nancy Day
In the class registration system (Wed's lecture), there
was an invariant to ensure the people could be on the
waiting list only if the class is full. It should be
(#enrolled < ClassLimit) <=> (waiting = <>)
cheers, nancy
CS245 Winter 2009 Instructor