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

allowed or estimated to be spend on certain works. We assume that the same
figures may exist in different budgets so budgets can be compared. Costs are
modelled as non-negative reals.
From a budget, we can observe the list (obs_BFl_B) as well as the set
(obs_BFs_B) of budget figures. Furthermore, we can observe the cost and sub-
budget of a given figure (obs_CF_B), we can calculate the total cost of a budget
(totalcost), and we assume that we can scale the costs of a budget (scale).
A budget is well-formed (wf_B) if and only if each cost is equal to the sum of
costs in the corresponding sub-budget; if such one exists. Furthermore, budget
figures must be unique.
We define an ordering on budgets after the following intuition. If a budget
(b 2 :B) only has a subset of figure compared to another budget (b 1 :B), we con-
sider it a specialization of the other budget; written b 2

b 1 . If a budget has
figures with lower costs compared to another budget with the same figures, the
former budget is a specialization of the latter. Furthermore, if a budget has a
figure which is broken down and a similar budget does not break down this
figure, the former budget is considered a specialization of the latter. Breaking
down a budget figure means that the figure having a cost aimed at a certain
range of applications, is restricted to a set of sub-figures having costs (in total)
aimed at a more narrow range of applications. Thereby, specialization of budgets
means narrowing the budget towards more specific applications. Generalization
is considered the opposite of specialization.
We define two operations meet and join for combining budgets. meet takes two
budgets and gives the combination which is a specialization of both argument
budgets. join takes two budgets and gives the combination which is a generaliza-
tion of both argument budgets. We shall not be concerned with whether the two
operations satisfy lattice criteria. In the definitions of the operations, we need
to consider that meet may take budgets without common figures. The result is,
however, not the empty map as we need the empty map to represent the most
general budget as well as sub-budgets for figures not broken down. Therefore, we
make a distinction between the most specialized budget (

≤

⊥ B :B) and the most

generalized budget ( B :B). Only the latter is modelled as the empty map. The

meet operation is special in the sense that when combining two budgets with
this operation, a figure in the one budget may put restrictions on the same figure
in the other budget. In the resulting budget we handle this by possibly scaling
the sub-figures proportionally such that the resulting budget is the most gen-
eral specialization of both argument budgets. The operation join is included for
completeness on and is not used further in this paper.

4.2 Formalization

type
B = BF m CF,

BF,
CF :: cost:C subbudget:B ,
C = {| c:Real • c ≥ 0.0 |} ,