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

value
meet: (Rn

m Q) × (Rn m Q) → (Rn m Q)

meet(rm,rm ) ≡

[ rn → q | rn:Rn,q:Q •

dom rm ∧
q=min(rm(rn),rm (rn)) ],

rn ∈ dom rm ∧ rn ∈

meets: (Rn m Q)-set → (Rn m Q)

meets(rms) ≡

if rms = {} then []

else
let rm:(Rn m Q) • rm ∈ rms in

meet(rm,meets(rms \{ rm } ))

end
end,

min: Q × Q → Q

min(q 1 ,q 2 ) ≡ if q 1 ≤ q 2 then q 1 else q 2 end,

join: (Rn m Q) × (Rn m Q) → (Rn m Q)

join(rm,rm ) ≡

[ rn → q | rn:Rn,q:Q •

dom rm ∧ q=rm(rn)+rm (rn)) (rn ∈ dom rm ∧ rn ∈ ∨

dom rm ∧ (rn ∈ dom rm ∧ rn ∈ q=rm(rn)) ∨

dom rm ∧ q=rm (rn)) ],

(rn ∈ dom rm ∧ rn ∈

m Q)-set → m Q)

joins: (Rn (Rn

≡
if rms =

joins(rms)

{}

then []

else
let rm:(Rn m Q) • rm ∈ rms in
join(rm,joins(rms \{ rm } ))
end
end,

≤ :(Rn m Q) × (Rn m Q) → Bool

rm 1 ≤ rm 2 ≡

dom(rm 1 )

⊆ dom(rm 2 ) ∧

( ∀ rn:Rn • rn ∈ dom(rm 1 ) ⇒ rm 1 (rn) ≤ rm 2 (rn))

6Pro tPans

A project plan is a planning instrument for structuring a collection of works to
be done and for stating the dependencies between and criteria of these works.