[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

How to model database tables?

Hi all. Played on and off with TLA+ over the years but really got a recent knowledge boost from the video series (thanks, Leslie).

I've decided to take an unfinished home project of making a PSP (personal software process) database system and model it in TLA+. In a nutshell, the system is:

The interesting (and undiscovered) part of the design is this:

Before I go too far down the wrong path, can someone tell me if my approach to modeling a single database table is correct (in this case a table of defect types)?

I chose to do a function from an "id" (say the primary key of a SQL table) to a "data" (the rest of the columns of a SQL table) or a constant indicating no row was found.

Hope you all had a great holidays. :)

Attachment: DefectType.tla
Description: Binary data