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

8.2 Galois Predicate

We now define a predicate stating that a given budget and a given project
plan relate to each other. That is, the budget designates (at least) the necessary
expenses for executing the project plan; and the project plan is executable within
these restrictions. We call this predicate the Galois predicate , formally defined
as:

value
φ :B WrkIdx) → × PP → (PrcIdx × Bool

φ (b,pp)(prcidx,wrkidx) ≡

( ∀ bf:BF • bf ⇒

sumcost(rel_map(pp,bf,wrkidx),prcidx)

∈ dom b

≤ cost(b(bf)) ∧

φ (subbudget(b(bf)),pp)(prcidx,wrkidx))
pre consistent(b,wrkidx) ∧ consistent(pp,wrkidx) ∧ consistent(pp,prcidx)

PrcIdx ∼ sumcost: ( Γ m (Rn m Nat)) × → C

sumcost(gm,prcidx) ≡

if gm = []then 0.0
else
let g: Γ • g dom gm in

sumcost (gm(g),prcidx) + sumcost(gm

∈

\{ g } ,prcidx)

end
end
pre ( ∀ rn ∈ dom rm ⇒ rn ∈ dom prcidx),

PrcIdx ∼ sumcost :(Rn m Nat) × → C

sumcost (rm,prcidx)

≡
if rm = []then 0.0
else
let rn:Rn • rn dom rm in

prcidx(rn)(rm(rn)) + sumcost (rm

∈

\{ rn } ,prcidx)

end
end
pre ( ∀ rn ∈ dom rm ⇒ rn ∈ dom prcidx)

The pre-condition is implied by the consistency predicates of φ . Note, that
the Galois predicate takes it origin in a quantification over budget figures. The
reason is due to the order in which budgets and project plans are created. That
is, usually it is the budget which restricts the project plans. Project plans are
made in a constructive way having budget knowledge in mind.
By means of the predicate φ , we can define the set of valid project plans, being
the project plans which each can be executed within a given budget; assuming
the mediating ties: