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

is_sumfigure: BF × B → Bool

is_sumfigure(bf,b) ≡

bf :BF •
bf ∈

( ∃

is_superior_BF(bf,bf ,b)),

∧

obs_BFs_B(b)

→

wf_B: B Bool

wf_B(b) ≡

unique_BF(b) ∧ checksubcost(b) ∧

( ∀ bf:BF • bf ∈ dom b ⇒ wf_B(b)),

checksubcost: B → Bool

checksubcost(b) ≡

b = ⊥ B ∧

( ∀ bf:BF • bf ⇒

cost(b(bf)) = totalcost(subbudget(b(bf)))),

∈ dom b

≤ :B × B → Bool

b 1 ≤ b 2 ≡

b 2 = B ∨

b 1 = ⊥ B ∨

(

b 1 = B ∧ dom(b 1 ) ⊆ dom(b 2 ) ∧

( ∀ bf:BF • bf ∈ dom(b 1 ) ⇒

cost(b 1 (bf)) ≤ cost(b 2 (bf)) ∧

subbudget(b 1 (bf)) ≤ subbudget(b 2 (bf)))

),

meet: B × B → B

meet(b 1 ,b 2 ) ≡

if b 1 = B then

b 2
elsif b 2 = B then

b 1
elsif dom b 1 ∩

dom b 2 = {} then

⊥ B
else
[ bf → mk_CF(c,bs) | bf:BF, c:C, bs:B •

(bf ∈ dom b 1 ∧ bf ∈ dom b 2 ∧

(subbudget(b 1 (bf)) = B ∧ subbudget(b 2 (bf)) = B ⇒

bs = B ∧

c = min(cost(b 1 (bf)), cost(b 2 (bf)))) ∧

(subbudget(b 1 (bf)) = B ∧ subbudget(b 2 (bf)) = B ∧

cost(b 1 (bf)) ⇒

bs = scale(subbudget(b 2 (bf)), cost(b 1 (bf))/cost(b 2 (bf)))

≤ cost(b 2 (bf))

∧