Designing Software with Predicate Logic
One reason I like teaching is it helps me understand things better. This came up in a couple different ways while working on the new book, and I’m too delighted by it not to share. Say we have the following user requirements:
Our conference center has a bunch of rooms that are reserved by people each day. Each room has a set of time slots that can be reserved. We need software that supports this.
That gives us three domain objects, Person, Room, and (time)Slot, and the concept of reservations. But there are many different ways our software could represent reservations:
All of these have their tradeoffs, and there’s a lot of factors you have to consider. One of these factors is correctness: do any representations make bugs less likely? And here’s where predicate logic can help. If the system diverges from the user requirements, that’s a bug, and we can use logic to formalize which requirements matter. First, let’s define the primitive predicate Reserved(p, r, s):
This is higher-level than any of our possible representations: for each one the implementation of Reserved in our code will look different, but the meaning is independent of our choice of structure. Now we can use this to define properties of the system. For example, the user might want that the same room and time can’t be reserved by two separate people simultaneously. In logic, we’d write that
