Can Alloy help with normal forms?

Questions
1

I’ve read a couple of blog posts on designing and changing database schemas:

Now, after making a draft of schema, can Alloy help with normal forms? Forgive my ignorance, I took a database course a long time ago.

As far as I understand, we take a table and start writing down functional dependencies explicitly. As shown above, Alloy can help with coming up with examples, so that we iteratively add more and more constraints that make sense.

Then we look at these constraints and figure out a list of functional dependencies. First, we check for 1NF, then 2NF, then 3NF. An example for 3NF taken from https://www.geeksforgeeks.org/third-normal-form-3nf/:

Functional dependency Set:
CAND_NO -> CAND_NAME
CAND_NO -> CAND_STATE
CAND_STATE -> CAND_COUNTRY
CAND_NO -> CAND_AGE

For the relation given here in the table, CAND_NO -> CAND_STATE and CAND_STATE -> CAND_COUNTRY are actually true. Thus, CAND_COUNTRY depends transitively on CAND_NO. This transitive relation violates the rules of being in the 3NF.

Can Alloy help with finding these violations?

1 Like
2

Never mind. After refreshing my memory on normal forms I realized the checking can be done mechanistically, when we have the list of functional dependencies. The hard part is understanding data and relations, and Alloy helps with that, as demonstrated in the links above.

1 Like