ObjectIdentity

Original bounded occurrence-renewal and explicit-reference teaching model; no full-source correspondence claim.

Package identity, input revision 1. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

successor · operator

identity · input revision 1 · CC0 1.0

successor == before.successors[before.reference]

Exact module download · Source bundle and reproduction instructions

after · operator

identity · input revision 1 · CC0 1.0

after == IF renew THEN
            [before EXCEPT !.live = Put(Without(@, {id}), successor, row),
                           !.past = Put(@, id, old), !.next = @ + 1,
                           !.successors = Put(@, id, successor)]
          ELSE [before EXCEPT !.live[id] = row]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: old, renew, row, successor, Put, Without

old · operator

identity · input revision 1 · CC0 1.0

old == before.live[id]

Exact module download · Source bundle and reproduction instructions

renew · operator

identity · input revision 1 · CC0 1.0

renew == NeedsRenewal(before, id, area, hidden)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NeedsRenewal

row · operator

identity · input revision 1 · CC0 1.0

row == [old EXCEPT !.area = area, !.position = position,
                          !.marks = IF renew THEN {} ELSE @]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: old, renew

successor · operator

identity · input revision 1 · CC0 1.0

successor == IF renew THEN before.next ELSE id

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: renew

Areas · operator

identity · input revision 1 · CC0 1.0

Areas == {"Display", "Private"}

Exact module download · Source bundle and reproduction instructions

CanFollowExplicitSuccessor · operator

identity · input revision 1 · CC0 1.0

CanFollowExplicitSuccessor(before) ==
    /\ before.reference \in DOMAIN before.successors
    /\ before.successors[before.reference] \in DOMAIN before.live

Exact module download · Source bundle and reproduction instructions

EmptyMap · operator

identity · input revision 1 · CC0 1.0

EmptyMap == [key \in {} |-> key]

Exact module download · Source bundle and reproduction instructions

FirstRow · operator

identity · input revision 1 · CC0 1.0

FirstRow == ObjectRow("item-a", "Display", 1, {"UseBound"})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectRow

FollowExplicitSuccessor · operator

identity · input revision 1 · CC0 1.0

FollowExplicitSuccessor(before) ==
    LET successor == before.successors[before.reference]
    IN [before EXCEPT !.reference = successor,
                      !.explicitLineage = Append(@, successor)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: successor

IdentityType · operator

identity · input revision 1 · CC0 1.0

IdentityType(before, maximum) ==
    /\ before.next \in 3..(maximum + 1)
    /\ DOMAIN before.live \subseteq 1..maximum
    /\ DOMAIN before.past \subseteq 1..maximum
    /\ \A id \in DOMAIN before.live : before.live[id] \in
           [physical : PhysicalItems, area : Areas, position : Positions, marks : SUBSET Marks]
    /\ \A id \in DOMAIN before.past : before.past[id] \in
           [physical : PhysicalItems, area : Areas, position : Positions, marks : SUBSET Marks]
    /\ DOMAIN before.successors \subseteq DOMAIN before.past
    /\ \A id \in DOMAIN before.successors : before.successors[id] \in 1..maximum
    /\ before.reference \in 1..maximum
    /\ before.explicitLineage \in Seq(1..maximum)
    /\ Len(before.explicitLineage) \in 1..maximum

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Areas, Marks, PhysicalItems, Positions

InitialIdentity · operator

identity · input revision 1 · CC0 1.0

InitialIdentity ==
    [live |-> [id \in {1, 2} |-> IF id = 1 THEN FirstRow ELSE StationaryRow],
     past |-> EmptyMap, next |-> 3, successors |-> EmptyMap,
     reference |-> 1, explicitLineage |-> <<1>>]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyMap, FirstRow, StationaryRow

LiveOccurrence · operator

identity · input revision 1 · CC0 1.0

LiveOccurrence(before, id) == id \in DOMAIN before.live

Exact module download · Source bundle and reproduction instructions

Marks · operator

identity · input revision 1 · CC0 1.0

Marks == {"UseBound"}

Exact module download · Source bundle and reproduction instructions

NeedsRenewal · operator

identity · input revision 1 · CC0 1.0

NeedsRenewal(before, id, area, hidden) == before.live[id].area # area \/ hidden

Exact module download · Source bundle and reproduction instructions

ObjectRow · operator

identity · input revision 1 · CC0 1.0

ObjectRow(physical, area, position, marks) ==
    [physical |-> physical, area |-> area, position |-> position, marks |-> marks]

Exact module download · Source bundle and reproduction instructions

PhysicalItems · operator

identity · input revision 1 · CC0 1.0

PhysicalItems == {"item-a", "item-b"}

Exact module download · Source bundle and reproduction instructions

PhysicalUniqueness · operator

identity · input revision 1 · CC0 1.0

PhysicalUniqueness(before) ==
    \A left, right \in DOMAIN before.live :
        before.live[left].physical = before.live[right].physical => left = right

Exact module download · Source bundle and reproduction instructions

Positions · operator

identity · input revision 1 · CC0 1.0

Positions == {1, 2}

Exact module download · Source bundle and reproduction instructions

Put · operator

identity · input revision 1 · CC0 1.0

Put(mapping, key, value) ==
    [index \in DOMAIN mapping \cup {key} |-> IF index = key THEN value ELSE mapping[index]]

Exact module download · Source bundle and reproduction instructions

RelocateObject · operator

identity · input revision 1 · CC0 1.0

RelocateObject(before, id, area, position, hidden) ==
    LET old == before.live[id]
        renew == NeedsRenewal(before, id, area, hidden)
        successor == IF renew THEN before.next ELSE id
        row == [old EXCEPT !.area = area, !.position = position,
                          !.marks = IF renew THEN {} ELSE @]
        after == IF renew THEN
            [before EXCEPT !.live = Put(Without(@, {id}), successor, row),
                           !.past = Put(@, id, old), !.next = @ + 1,
                           !.successors = Put(@, id, successor)]
          ELSE [before EXCEPT !.live[id] = row]
    IN [state |-> after, successor |-> successor, renewed |-> renew]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: after, renew, successor

ResolveReference · operator

identity · input revision 1 · CC0 1.0

ResolveReference(before, id) ==
    IF LiveOccurrence(before, id) THEN before.live[id] ELSE "NoLiveObject"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LiveOccurrence

StationaryRow · operator

identity · input revision 1 · CC0 1.0

StationaryRow == ObjectRow("item-b", "Display", 2, {})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectRow

Without · operator

identity · input revision 1 · CC0 1.0

Without(mapping, keys) == [key \in DOMAIN mapping \ keys |-> mapping[key]]

Exact module download · Source bundle and reproduction instructions