形式制約の書き方例
テーブル名tに対して、tの（ある時点での）インスタンス＝状態を{|t|}と書く。
- 学生テーブル = ('学生', {'番号':int, '氏名':string})
- 授業テーブル = ('授業', {'番号':int, '名前':string})
- 受講テーブル = ('受講', {'授業':int, '学生':string})
別名関係（意味的注釈のひとつ）
- {学生.氏名 = 受講.学生, 授業.番号 = 受講.授業}
制約
- 同姓同名の学生はいない ∀s, t∈{|学生|}.( s[氏名] ≠ t[氏名] ⇒ s[番号] ≠ t[番号] )
- 受講している学生が実在する ∀x∈{|受講|}.∃s∈{|学生|}.( x[学生] = s[氏名] )
- 受講している授業が実在する ∀x∈{|受講|}.∃c∈{|授業|}.( x[授業] = c[番号] )
このとき、同じ氏名で異なる番号のレコードを挿入すると制約が満たされなくなる。学生テーブルのレコードだけ、授業テーブルのレコードだけ削除すると、制約が満たされなくなる。
やることは、
- 制約を変えることができないなら、"山田太郎2"のような名前を使う。
- 人手で、辻褄が合うように削除する。
背後にある問題点は、
- 「同姓同名の学生はいない」が現実的妥当性を持たなかった。
- 単一テーブルに対する生のdeleteコマンドが、許容コマンドではなかった。
システム的に実現できる制約は、
