Information Technology Reference
In-Depth Information
3. create - The function takes two identifiers and declares a new channel vari-
able (type iType ) using the first identifier, to be owned by the member rep-
resented by the second identifier. The precondition requires that the member
is registered and the variable identifier does not exist in the state.
value
create: Id × Id × State StateX
create(cid, mid, s)
let x1 = make(new(cid, iType, mid)) in decl(x1) end
pre eval(canCreate(cid, mid), s),
canCreate: Id × Id BoolX
canCreate(chid, id)
let x = hasPart(make(idCat, id2val(id)), get(reg))
in and(x, not(hasVar(get(chid)))) end
4. destroy - The function takes two identifiers as arguments and undeclares
the variable represented by the first identifier. The precondition is that the
variable exists in the state, that the second identifier represents the owner
of the variable, and that the variable contains only two id -category parts -
its own identifier and the owner identifier.
value
destroy: Id × Id × State StateX
destroy(cid, mid, s)
undecl(cid) pre eval(canDestroy(cid, mid), s),
canDestroy: Id × Id BoolX
canDestroy(cid, mid)
let
x1 = hasVar(get(cid)),
x2 = equal(parts(get(cid), idCat), n(2)),
x3 = hasVal(get(get(cid), idCat, make(n(2))), id2val(mid))
in and(x1, and(x2, x3)) end
5. subscribe - The function takes two identifiers - channel variable and mem-
ber subscriber. It creates an id -category part with the new subscriber value,
and adds this part to the channel variable. The precondition is that sub-
scriber and channel exists, and channel variable does not contain such part.
value
subscribe: Id × Id × State StateX
subscribe(cid, mid, s)
change(cid, add(make(idCat, id2val(mid)), get(cid)))
pre eval(canSubscribe(cid, mid), s),
canSubscribe: Id × Id BoolX
canSubscribe(cid, mid)
let
x1 = hasVar(get(mid)),
x2 = hasVar(get(cid)),
x3 = hasPart(make(idCat, id2val(mid)), get(cid))
in and(x1, and(x2, not(x3))) end
Search WWH ::




Custom Search