Formalization and Verification of Relational Database Normal Forms Using the Gamma Framework

The General Abstract Model for Multi-set mAnipulation (GAMMA) is a parallel computational and programming paradigm. It utilizes the multi-set data structure and a program structure that is defined as a pair of . The elements of the multi-sets are consumed in successive chemical reactions to produce new elements according to a set of conditions. In this paper, we exploit the expressiveness of Gamma to elegantly and succinctly specify the normalization aspects in relational databases and use its computational power to achieve greater performance in verifying and realizing relational database normal forms. We present two approaches in database designs and discuss the performance of Gamma on the extensive computation involved in the relational database normalization process.