SQL
PostgreSQL

SQLを学びます(8) データベースの設計法(2)

More than 1 year has passed since last update.

前回の続き。

データベースの仕様

前回に定めたデータベースの仕様を再掲。
状態遷移に関する制約の実装は後ほど考えることにするので今は省略。

ドメイン

\mathrm{ENO} \buildrel\mathrm{def}\over= \left\{ n \in \mathbb{Z} : 1 \le n \le 999 \right\}
\\
\mathrm{ENAME} \buildrel\mathrm{def}\over= \left\{ s \in \mathbb{S} : 1 \le \#s \le 10 \right\}
\\
\mathrm{JOB} \buildrel\mathrm{def}\over= \left\{ \textrm{'PRESIDENT', 'ADMINISTRATOR', 'CLERK'} \right\}
\\
\mathrm{SAL} \buildrel\mathrm{def}\over= \left\{ n \in \mathbb{Z} : 1 \le n \le 10000 \right\}
\\
\mathrm{DNO} \buildrel\mathrm{def}\over= \left\{ n \in \mathbb{Z} : 1 \le n \le 99 \right\}
\\
\mathrm{DNAME} \buildrel\mathrm{def}\over= \left\{ s \in \mathbb{S} : 1 \le \#s \le 10 \right\}
\\
\mathrm{LOC} \buildrel\mathrm{def}\over= \left\{ s \in \mathbb{S} : 1 \le \#s \le 6 \right\}

タプル宇宙

\mathrm{T\_Emp} \buildrel\mathrm{def}\over= \left\{ e \in \Pi\left\{ \begin{array}{l}
    (\mathrm{eno}, \mathrm{ENO}), \\
    (\mathrm{ename}, \mathrm{ENAME}), \\
    (\mathrm{job}, \mathrm{JOB}), \\
    (\mathrm{sal}, \mathrm{SAL}), \\
    (\mathrm{dno}, \mathrm{DNO})
\end{array} \right\} : \mathrm{CX\_T\_Emp}_1(e) \right\}
\\
\mathrm{T\_Dep} \buildrel\mathrm{def}\over= \Pi\left\{ (\mathrm{dno}, \mathrm{DNO}), (\mathrm{dname}, \mathrm{DNAME}), (\mathrm{loc}, \mathrm{LOC}), (\mathrm{mgr}, \mathrm{ENO}) \right\}

ここで、

\mathrm{CX\_T\_Emp}_1(e) \buildrel\mathrm{def}\over\equiv e\;\mathrm{job} = \textrm{'PRESIDENT'} \Rightarrow 5000 \le e\;\mathrm{sal}

関係宇宙

\mathrm{R\_Emp} \buildrel\mathrm{def}\over= \left\{ E \in \wp\;\mathrm{T\_Emp} : \mathrm{CX\_R\_Emp}_1(E) \wedge \mathrm{CX\_R\_Emp}_2(E) \wedge \mathrm{CX\_R\_Emp}_3(E) \right\}
\\
\mathrm{R\_Dep} \buildrel\mathrm{def}\over= \left\{ D \in \wp\;\mathrm{T\_Dep} : \mathrm{CX\_R\_Dep}_1(D) \wedge 
\mathrm{CX\_R\_Dep}_2(D) \right\}

ここで、

\mathrm{CX\_R\_Emp}_1(E) \buildrel\mathrm{def}\over\equiv \left\langle \forall e_1, e_2 \in E : e_1\;\mathrm{eno} = e_2\;\mathrm{eno} : e_1 = e_2 \right\rangle
\\
\mathrm{CX\_R\_Emp}_2(E) \buildrel\mathrm{def}\over\equiv \#\left\{ e \in E : e\;\mathrm{job} = \textrm{'PRESIDENT'} \right\} \le 1
\\
\mathrm{CX\_R\_Emp}_3(E) \buildrel\mathrm{def}\over\equiv \left\langle \forall d \in E \Downarrow \{ \mathrm{dno} \} : \left\langle \exists e \in E : e\;\mathrm{dno} = d\;\mathrm{dno} : e\;\mathrm{job} \in \left\{ \textrm{'PRESIDENT', 'ADMINISTRATOR'} \right\} \right\rangle
    \\ : \left\langle \exists e \in E : e\;\mathrm{dno} = d\;\mathrm{dno} : e\;\mathrm{job} = \textrm{'CLERK'} \right\rangle \right\rangle
\\
\mathrm{CX\_R\_Dep}_1(D) \buildrel\mathrm{def}\over\equiv \left\langle \forall d_1, d_2 \in D : d_1\;\mathrm{dno} = d_2\;\mathrm{dno} : d_1 = d_2 \right\rangle
\\
\mathrm{CX\_R\_Dep}_2(D) \buildrel\mathrm{def}\over\equiv \left\langle \forall d_1, d_2 \in D : d_1\downarrow\{\mathrm{dname}, \mathrm{loc}\} = d_2\downarrow\{\mathrm{dname}, \mathrm{loc}\} : d_1 = d_2 \right\rangle

データベース宇宙

\mathrm{U\_Comp} \buildrel\mathrm{def}\over= \left\{ s \in \Pi\left\{ \begin{array}{l}
    (\mathrm{Emp}, \mathrm{R\_Emp}), \\
    (\mathrm{Dep}, \mathrm{R\_Dep})
\end{array} \right\}  : \begin{array}{l}
    \mathrm{CX\_U\_Comp}_1(s\;\mathrm{Emp}, s\;\mathrm{Dep}) \\
    \wedge \mathrm{CX\_U\_Comp}_2(s\;\mathrm{Dep}, s\;\mathrm{Emp}) \\
    \wedge \mathrm{CX\_U\_Comp}_3(s\;\mathrm{Emp}, s\;\mathrm{Dep})
\end{array} \right\}

ここで、

\mathrm{CX\_U\_Comp}_1(\mathrm{Emp}, \mathrm{Dep}) \buildrel\mathrm{def}\over\equiv \left\{ e\;\mathrm{dno} : e \in \mathrm{Emp}
 \right\} \subseteq \left\{ d\;\mathrm{dno} : d \in \mathrm{Dep} \right\}
\\
\mathrm{CX\_U\_Comp}_2(\mathrm{Dep}, \mathrm{Emp}) \buildrel\mathrm{def}\over\equiv \left\{ d\;\mathrm{mgr} : d \in \mathrm{Dep} \right\} \subseteq \left\{ e\;\mathrm{eno} : e \in \mathrm{Emp} \wedge e\;\mathrm{job} \ne \textrm{'PRESIDENT'} \right\}
\\
\mathrm{CX\_U\_Comp}_3(\mathrm{Emp}, \mathrm{Dep}) \buildrel\mathrm{def}\over\equiv \left\langle \forall e \in \mathrm{Emp} :: \left\langle \forall d \in \mathrm{Dep} : d\;\mathrm{mgr} = e\;\mathrm{eno} : d\;\mathrm{dno} = e\;\mathrm{dno} \right\rangle \right\rangle

PostgreSQLでの実装

話を簡単にするためにトランザクション分離レベルはひとまずSERIALIZABLEとする。
上記の仕様を満たす実装は次のようになるが、まだまだ効率化できるのでそれを次回から考えていくことにする。
制約チェックの遅延についても考えていく必要がある。

CREATE DOMAIN ENO AS INT NOT NULL CHECK (VALUE BETWEEN 1 AND 999);
CREATE DOMAIN ENAME AS VARCHAR(10) NOT NULL CHECK (1 <= LENGTH(VALUE));
CREATE DOMAIN JOB AS VARCHAR(13) NOT NULL CHECK (VALUE IN ('PRESIDENT', 'ADMINISTRATOR', 'CLERK'));
CREATE DOMAIN SAL AS INT NOT NULL CHECK (VALUE BETWEEN 1 AND 10000);
CREATE DOMAIN DNO AS INT NOT NULL CHECK (VALUE BETWEEN 1 AND 99);
CREATE DOMAIN DNAME AS VARCHAR(10) NOT NULL CHECK (1 <= LENGTH(VALUE));
CREATE DOMAIN LOC AS VARCHAR(6) NOT NULL CHECK (1 <= LENGTH(VALUE));


CREATE TABLE Emp(
    eno ENO CONSTRAINT CX_R_Emp_1 UNIQUE,
    ename ENAME,
    job JOB,
    sal SAL,
    dno DNO,
    CONSTRAINT CX_T_Emp_1 CHECK (job <> 'PRESIDENT' OR 5000 <= sal)
);

CREATE TABLE Dep(
    dno DNO CONSTRAINT CX_R_Dep_1 UNIQUE,
    dname DNAME,
    loc LOC,
    mgr ENO,
    CONSTRAINT CX_R_Dep_2 UNIQUE(dname, loc)
);

ALTER TABLE Emp ADD CONSTRAINT CX_U_Comp_1 FOREIGN KEY (dno) REFERENCES Dep(dno);


CREATE OR REPLACE FUNCTION CX_R_Emp_2() RETURNS TRIGGER AS $$
BEGIN
    IF 1 < (SELECT COUNT(*) FROM Emp WHERE job = 'PRESIDENT') THEN
        RAISE EXCEPTION 'CX_R_Emp_2 violation';
    END IF;
    RETURN NULL;
END;
$$ LANGUAGE plpgsql;

CREATE TRIGGER CX_R_Emp_2 AFTER INSERT OR UPDATE OF job ON Emp
    FOR EACH STATEMENT EXECUTE PROCEDURE CX_R_Emp_2();


CREATE OR REPLACE FUNCTION CX_R_Emp_3() RETURNS TRIGGER AS $$
BEGIN
    IF EXISTS (SELECT d.dno FROM Emp d WHERE EXISTS (SELECT e1.* FROM Emp e1 WHERE e1.dno = d.dno AND e1.job IN ('PRESIDENT', 'ADMINISTRATOR'))
                                                AND NOT EXISTS (SELECT e2.* FROM Emp e2 WHERE e2.dno = d.dno AND e2.job = 'CLERK')) THEN
        RAISE EXCEPTION 'CX_R_Emp_3 violation';
    END IF;
    RETURN NULL;
END;
$$ LANGUAGE plpgsql;

CREATE TRIGGER CX_R_Emp_3 AFTER INSERT OR UPDATE OF dno, job OR DELETE ON Emp
    FOR EACH STATEMENT EXECUTE PROCEDURE CX_R_Emp_3();


CREATE OR REPLACE FUNCTION CX_U_Comp_2() RETURNS TRIGGER AS $$
BEGIN
    IF EXISTS (SELECT d.* FROM Dep d WHERE NOT EXISTS (SELECT e.* FROM Emp e WHERE d.mgr = e.eno AND e.job <> 'PRESIDENT')) THEN
        RAISE EXCEPTION 'CX_U_Comp_2 violation';
    END IF;
    RETURN NULL;
END;
$$ LANGUAGE plpgsql;

CREATE TRIGGER CX_U_Comp_2 AFTER UPDATE OF eno, job OR DELETE ON Emp
    FOR EACH STATEMENT EXECUTE PROCEDURE CX_U_Comp_2();

CREATE TRIGGER CX_U_Comp_2 AFTER INSERT OR UPDATE OF mgr OR DELETE ON Dep
    FOR EACH STATEMENT EXECUTE PROCEDURE CX_U_Comp_2();