Subsection 6.2.11 Specifications for a Business Application
So now we’ve talked about:
Writing logical expressions that describe constraints on values in application databases.
Writing logical expressions that describe the functions that programs should perform.
Let’s combine these two things.
Up until now, when we did (1), we mostly assumed that people were doing the work. The logical constraints just checked them. So, for example, people assigned employees to projects and to supervisors. The constraints made sure that they did so in an acceptable way.
But now suppose that we want to write a program to do a similar sort of task. Now we can write the same kinds of constraints but we’ll treat them as program specifications. The job of the program is to make the constraints true.
Suppose that we want to schedule classes into classrooms. In a large university, this is a huge task, generally made worse by the fact that there’s little latitude: there may be only barely enough classrooms to go around and then only if some classes happen at undesirable times like 8:00 in the morning. The program that does this may have to try a lot of different assignments before it finds one that works. We’re not going to try to describe how it should do that. All we’re going to do is to describe what an acceptable solution is. Once the program finds such a solution, it can stop.
Define:
Class(x): True if x is a class.
Room(r): True if r is a room
Timeslot(t): True if t is a time slot
Scheduled(c, r, t): True if c is scheduled in room r in time slot t.
size(c): Returns the number of students in class c.
capacity(r): Returns the capacity of room r.
Here’s a first attempt at a specification for a scheduling program. We’ll require that every class be scheduled (at some time and in some large enough room). We can say that with this expression:
[1] \(\forall \)c ( \(\exists\)r, t (Room(r) \(\wedge \) Timeslot(t) Scheduled(c, r, t) \(\wedge \) (size(c) \(\leq \) capacity(r))))
This appears to be a good start. But closer inspection reveals several problems. Can you spot some of them? We’ll work on fixing them as an exercise.
Exercises Exercises
1.
1. Recall that we are trying to write a specification for a class scheduling program. We’ve defined:
Class(x): True if x is a class.
Room(r): True if r is a room
Timeslot(t): True if t is a time slot
Scheduled(c, r, t): True if c is scheduled in room r in time slot t.
size(c): Returns the number of students in class c.
capacity(r): Returns the capacity of room r.
Our first attempt was:
[1] ∀c ( ∃r, t (Room(r) ∧ Timeslot(t) ∧ Scheduled(c, r, t) ∧ (size(c) ≤ capacity(r))))
But we observe that we can satisfy this constraint by scheduling all classes at the same time in the same room. Oops. We need to add a new requirement that says that a given room, at a given time slot, may be assigned to no more than one class.
Consider the following statements. Read each of these as saying that we require [1] above and a new conjunct. Which (one or more) of them correctly captures our requirement?
I. [1] ∧ ∀r (Room(r) → ∃t (¬∃d (∃e ((d ≠ e) ∧ Scheduled(d, r, t) ∧ Scheduled(e, r, t)))))
II. [1] ∧ ∀r (Room(r) → ¬∃t (∃d (∃e ((d ≠ e) ∧ Scheduled(d, r, t) ∧ Scheduled(e, r, t)))))
III. [1] ∧ ∀t (∀r, d, e ((Room(r) ∧ Scheduled(d, r, t) ∧ Scheduled(e, r, t)) → (d = e)))
2.
2. Recall that we are trying to write a specification for a class scheduling program. We’ve defined:
Class(x): True if x is a class.
Room(r): True if r is a room
Timeslot(t): True if t is a time slot
Scheduled(c, r, t): True if c is scheduled in room r in time slot t.
size(c): Returns the number of students in class c.
capacity(r): Returns the capacity of room r.
After our second attempt, we had:
[1] ∀c ( ∃r, t (Room(r) ∧ Timeslot(t) ∧ Scheduled(c, r, t) ∧ size(c) ≤ capacity(r))))
∧
[2] ∀r (Room(r) → ¬∃t (∃d (∃e ((d ≠ e) ∧ Scheduled(d, r, t) ∧ Scheduled(e, r, t)))))
Now every class must be scheduled [1] and no two classes may be scheduled in the same room at the same time [2].
But we’ve still got a problem. Nothing prevents the scheduler from scheduling a class at more than one time or in more than one room. It probably wouldn’t want to, but strange things happen in complicated programs and we certainly don’t want to allow this. So we need to add another constraint.
Consider the following statements. Read each of these as saying that we require [1] and [2] above and a new conjunct. Which (one or more) of them correctly captures our requirement?
I. [1] ∧ [2] ∧ ∀c, r, s, t, w ((Scheduled(c, r, t) ∧ Scheduled(c, s, w)) → ((r = s) ∧ (t = w))
II. [1] ∧ [2] ∧ ¬∃r (∃c, s, t, w (Scheduled(c, r, t) ∧ Scheduled(c, s, w)) ∧ ((r ≠ s) ∨ (t ≠ w))
III. [1] ∧ [2] ∧ ¬∃t (∃c, r, s, w (Scheduled(c, r, t) ∧ Scheduled(c, s, w)) ∧ ¬((r = s) ∧ (t = w))
Just I.
Just II.
Just III.
Just II and III.
All three.