r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope
On this page

Objects and lifetime

A rule that targets “object 7” needs to say which object that name identifies and how long the reference remains valid. An object can leave a zone, cease to exist as a live object, or acquire a successor. Those changes need explicit policies; a matching title or physical piece cannot decide them by itself.

The values and state chapter introduces sets, records and keyed mappings. Here those values describe identity and references.

Distinguish a physical item from its live appearance

A physical component can have a stable identity across a match. Its current appearance in the modeled world can have a separate live identity. For example, the same physical item may leave a location and later return under a rule that creates a fresh live object.

Identity

Question it answers

Physical identity

Which enduring component is this?

Live identity

Which current object does this state record?

Historical reference

Which earlier object or event did this record concern?

The separation permits a model to retain history without pretending that a retired object is still live. It also prevents a newly created object from inheriting an old target merely because it uses the same physical component.

Give references an existence condition

Suppose objects maps each live identity to its record. This notation fragment tests whether identity 7 is live:

7 \in DOMAIN objects

A target can require both existence and eligibility: the object must be live, in an allowed location and of a permitted kind. Existence alone does not make it a legal target. A target accepted earlier may need another check before resolution if intervening changes can make it ineligible.

For a concrete reading example, an announcement targets live object 7. That object is retired, and the same physical item later returns as live object 12. The original reference still names 7. It does not automatically change to 12.

If a procedure is meant to follow a successor, its contract must say so and define the correspondence. A deliberate successor reference and a stale reference are different cases.

The teaching package makes that lookup explicit. ResolveReference returns a current occurrence only while the reference belongs to the live mapping:

identity · input revision 1 · CC0 1.0

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

Definition and resolved references · Exact module download · Source bundle and reproduction instructions

For movement, follow RelocateObject and its NeedsRenewal guard. Deliberate rebinding uses FollowExplicitSuccessor. These links lead to the exact prepared definitions and their dependencies.

Make creation and retirement precise

An allocation contract needs an available identity, a complete new object record and explicit frame conditions for existing objects. A retirement contract needs to remove the live entry while retaining any required historical information.

Useful safety questions include:

  • Can two live objects acquire the same identity?

  • Can creation overwrite an existing live record?

  • Can a historical reference begin naming a different object through identity reuse?

  • Can an unrelated object change during a movement or retirement?

Freshness depends on the model’s actual identity policy. Choosing a key absent from the current live mapping is not sufficient if a retired key can still occur in history. A finite checking domain also needs a stated allocation bound; running out of test identities is not a game rule unless the mechanism says it is.

Keep relationships separate from identity

Ownership, control, execution and hosting describe relationships involving an object. They are not interchangeable names for the object itself. A control change can preserve live identity while changing which participant may use an ability. A host change can preserve identity while changing a direct relationship.

Likewise, a direct host and an ancestor in a hosting chain are different facts. If a rule follows the chain, it needs a defined traversal and a way to handle invalid relationships. If it uses only the immediate host, a broader traversal would change its meaning.

Information has its own lifetime

A participant can know an object’s identity temporarily without moving it or changing its activity. That knowledge may expire at a specified boundary or be invalidated by a particular movement. The rule must identify the observer, the object reference, the information granted and its expiry.

Knowing an earlier live object does not automatically reveal a newly created successor. Conversely, a movement policy may deliberately retain knowledge. Read the particular transition and observation contract rather than assuming either outcome.

These local conditions do not establish that all concealed information remains protected across every interaction. That requires a separate observation property and its own evidence.

The identity evidence records the finite teaching profile with occurrence identifiers 1–4 and the deliberately defective implicit-follow companion. Read its bounds and properties alongside these definitions. It does not establish the broader hosting, control or information-flow obligations discussed above. Continue with priority and completion, where references also identify the exact procedure waiting to resume.