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

b:B • wf_B(b) B = {| |}

value
[ instanses ]
B :B= [],
⊥ B :B,

[ observer functions ]
obs_BFl_B: B BF ∗ , →

obs_BFs_B: B → BF-set,

BF →

obs_CF_B: B CF

post obs_CF_B(b,bf) as cf
pre bf

×

∈ obs_BFs_B(b),

totalcost: B ∼

→ C

totalcost(b) ≡

if b = B then 0.0

else let bf:BF • bf dom b in

cost(b(bf)) + totalcost(b

∈

\{ bf } )

end

end
pre b = ⊥ B ,

[ misc ]
scale: B

× →

Real B

≡

scale(b,r)

→ |

[ bf mk_CF(c,bs) bf:BF, c:C, bs:B •

bf ∈ dom b ∧
c = r ∗ cost(b(bf)) ∧
bs = scale(subbudget(b(bf)),r) ],

min: C × C → C

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

max: C × C → C

max(c 1 ,c 2 ) ≡ if c 1 ≥ c 2 then c 1 else c 2 end,

[ predicates ]
unique_BF: B → Bool

unique_BF(b) ≡

len obs_BFl_B(b) = card obs_BFs_B(b),

is_superior_BF: BF × BF × B → Bool,

is_subordinary_BF: BF × BF × B → Bool,