155 Denotation Examples

The examples below focus on the result R and formula Ψ parts of path-frame denotations. The free-variable set F is part of the frame, but is omitted from these compact examples when it is clear from the displayed result and formula.

Path Result Formula 
s.supplier
 
supplier = S:Supplier
 
s.supplier(S)
 
s.supplier.name
 
name = N:String
 
∃S:Supplier
  s.supplier(S)
  ∧ S.name(N)
 
s.shipment.(
  supplier.name as sname,
  part.name as pname,
  qty
)
 
sname = SN:String,
pname = PN:String,
qty = Q:Integer
 
∃SP:Shipment
∃S:Supplier
∃P:Part
  s.shipment(SP)
  ∧ SP.supplier(S)
  ∧ S.name(SN)
  ∧ SP.part(P)
  ∧ P.name(PN)
  ∧ SP.qty(Q)
 
s.supplier.
  (status*rating)
 
_anon_ = T*Q:Real
 
∃S:Supplier
  s.supplier(S)
  ∧ S.status(T)
  ∧ S.rating(Q)

Prism coloring

The following examples use this small schema: 

value Prism
{
    Real width;
    Real height;
    Real depth;
}

value Sphere
{
    Real radius;
}

variant Shape
{
    Prism prism;
    Sphere sphere;
}

enum Color
{
    red, green, blue
}

entity Object
{
    Shape shape;
    Color color;
}

entity Inventory
{
    Object object*;
}
Prism Shape
Path Result Formula 
i.object.
  shape.prism
 
prism = P:Prism
 
∃O:Object
∃S:Shape
  i.object(O)
  ∧ O.shape(S)
  ∧ S.prism(P)
Red Or Green Prisms
Path Result Formula 
i.object.[
  shape.prism.Σexists
  ∧ (color.red
     ∨ color.green)
]
 
object = O:Object
 
i.object(O)
∧ ∃S:Shape
  ∃P:Prism
  O.shape(S)
  ∧ S.prism(P)
∧ ∃C:Color
  O.color(C)
  ∧ (
    ∃U:{} C.red(U)
    ∨ ∃V:{} C.green(V)
  )