Relating Domain Concepts Intensionally by Ordering Connections - Formal Methods and Hybrid Real-Time Systems - page 206

to the smallest quantity. join gives the project plan for which each node is in
either argument project plans. For each such node, the set of object aspects is
the union set and the resource usage maps resource types present in either nodes
to the largest quantity. join is included for completeness only and is not used
further in this paper. Due to the abstraction of using observer functions, the two
operations are defined implicitly.

6.2 Formalization

type
PP = Γ

m Γ -set,
PP = {| pp:PP • wf_PP(pp) |}
Γ ,

value
obs_On_ Γ : Γ PP →

On
post obs_On_ Γ (g,pp) as on
pre g

×

dom pp,
obs_Xs_ Γ : Γ

∈

× PP → X-set,

obs_Rn_ Γ : Γ × PP → Rn-set,

obs_Rm_ Γ : Γ × PP → (Rn m Q),

obs_rel_res: Γ × X × PP → (Rn m Q)

axiom g: Γ , pp:PP •

obs_Rn_ Γ (g,pp)

∀

≡ dom obs_Rm_ Γ (g,pp),

obs_Rm_ Γ (g,pp) ≡

meets( { rm | rm:(Rn m Q) •

( ∃ x:X • x ∈ obs_Xs_ Γ (g,pp) ⇒ rm=obs_rel_res(g,x,pp)) } )

value
wf_PP: PP

→

Bool

wf_PP(pp) ≡
( ∀ gs: Γ -set • gs ∈ rng pp ⇒ gs ⊆ dom pp) ∧
( ∀ g: Γ • g ∈ dom pp ⇒
g ∈{ g_succ | g_succ: Γ

• is_before(g,g_succ)(pp)

} ),

is_before: Γ × Γ → PP → Bool

is_before(g,g )(pp) ≡

g ∈ pp(g) ∨

g : Γ • g ∈ is_before(g ,g )(pp)), ( ∃ pp(g) ∧

meet: PP PP

meet(pp 1 ,pp 2 ) as pp
post pp =[g

× PP →

→ gs g: Γ ,gs: Γ -set •

g

|

∈ dom pp 1 ∧ g ∈ dom pp 2 ∧