interval characterization proofs and worked examples

1 files changed, 35 insertions, 0 deletions

diff --git a/examples/integrity.sol b/examples/integrity.sol
new file mode 100644
index 0000000..2729f4b
--- /dev/null
+++ b/examples/integrity.sol
@@ -0,0 +1,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]