aboutsummaryrefslogtreecommitdiffstats
path: root/examples/integrity.sol
blob: 2729f4bf5c88be7151f1101fdb6a573f90ef9eff (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
% Schemas constrain by membership: primitive domains, refinements,
% and foreign keys are one mechanism. A program whose facts violate
% them gets no world at all; this one is admitted.

Relation named: Department schema: #(
  [id domain: Integer]
  [title domain: String]
)

[Department id: 1 title: "Engineering"]
[Department id: 2 title: "Design"]

Relation named: Employee schema: #(
  [name domain: String]
  % A foreign key is a membership criterion, nothing more special.
  % Only the subject D is free; other attributes stay existential.
  [dept domain: ([Department id: D])]
  % A refinement: a natural at most 100.
  [score domain: ([Natural value: S] :and [LessThanEqual left: S right: 100])]
)

[Employee name: "Marcos" dept: 1 score: 90]
[Employee name: "Ana" dept: 2 score: 75]

Query expression: [Employee name: N dept: D score: S]

% Join through the foreign key.
Query expression:
  [Employee name: N dept: D score: S] :and
  [Department id: D title: T]

% Try it yourself: append one of these lines and watch admission
% reject the whole program.
%   [Employee name: "Ghost" dept: 9 score: 50]
%   [Employee name: "Over" dept: 1 score: 101]