The Omega Coffee Club has the following formal specification.
It is indeed used to compute memberships and payments.
The program runs on CP.
When CP executes the specification, CP is in mode
President-of-the-Omega-Coffee-Club.
Then please do not ask CP for any special treatment because in this mode CP
is not able to execute any non-specified procedure like being nice, giving
coffee to non-members, making any special offers, or discussing the rules of
the coffee club. Thank you very much indeed for your understanding.
b\in\N; (*cash in cup-of-coffee currency*)
k\in\N; (*number of cups of coffee
that can be brewed from the coffee in stock*)
V : set (*members*)
d : V->\N (*drunken coffee per member*)
g\in\N_+; (*basic membership investment*)
m\in\N; (*investment factor*)
s\in\N. (*sponsoring*)
The invariant of the complete stocks holds:
b + k + \sum_{i\in V} d_i == \card(V) * g * m + s
INITIALIZATION s = m = k = b = 0; V = \emptyset;
DRINK(i) (*i\in V; 0<=k*) d_i++; k--;
BUY-COFFEE(x) (*x<=b*) b -= x; k += x;
INCREASE-OF-INVESTMENT b += \card(V) * g; m++;
ASK-TO-PAY (*V\not=\emptyset*)
i = \varepsilon j\in V. \forall k\in V. d_k <= d_j; b += d_i; d_i = 0;
JOIN(i) (*i\notin V*) V \cup= \{i\}; d_i = 0; b += g * m;
LEAVE(i) (*i\in V*) V \setminus= \{i\}; b -= g * m - d_i;
SPONSORING(x) b += x; s += x;
On Fairness:
Nobody can drink more coffee than b + k.
Then he will be asked to pay either by INCREASE-OF-INVESTMENT
or ASK-TO-PAY or to get some SPONSORING.
Since nobody lives longer than 10000000000 cups,
final justice will be achieved by LEAVE.