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

Price indices concern project plans. Consistency here means that the unit cost
function of the price index, is defined for all resource types referred to in the
project plan.

value
consistent: PP

× PrcIdx → Bool

consistent(pp,prcidx) ≡

( ∀ rn:Rn •

( ∃ g: Γ • g ∈ dom pp ∧ rn ∈ obs_Rn_ Γ (g,pp)) ⇒ rn ∈ dom prcidx)

We shall assume that the unit cost function is complete such that it (some
way or another) covers the quantities necessary. Also, we shall assume that any
quantity discount is handled by the price index itself.

8 The Characteristics Connection

In this section, we shall define the characteristics connection ; i.e., a Galois con-
nection between budgets and project plans.

8.1 Identifying Abstract Properties
As a first step, we need to define the abstract properties of budgets. For doing
so, we need the following definition:
Definition 11 (Relevant Nodes). A node in a project plan is relevant with
respect to a given budget figure, if and only if there exists an object aspect of the
node such that the work given by the operation of the node and the object aspect,
is mapped to the budget figure in the work index.
Formally, we write:

value
rel_nds: PP × BF × WrkIdx → Γ -set

rel_nds(pp,bf,wrkidx) ≡

{ g | g: Γ

•

g ∈ dom pp ∧

( ∃ x:X • x ∈ obs_Xs_ Γ (g) ∧ bf=wrkidx(obs_On_ Γ (g),x)) }

The mapping from relevant nodes to relevant resource usage (see Sect. 10) is
defined as a variant of rel_nds:

value
rel_map: PP

× BF × WrkIdx → ( Γ m (Rn m Q))

rel_map(pp,bf,wrkidx) ≡

[ g → rm | g: Γ ,rm:(Rn m Q) •

g ∈ rel_nds(pp,bf,wrkidx) ∧

( ∃ x:X • x ∈ obs_Xs_ Γ (g) ∧ bf=wrkidx(obs_On_ Γ (g),x) ∧

rm=obs_rel_res(g,x)) ],