ObjectCreated

Mattias Ulbrich sent this after the JML Dagstuhl seminar (his email dated July 21, 2009).

on Friday we have talked about how we can manifest the "\created" feature in the reference manual. ...

I intend to add after 11.4.21 the following section:

---

The syntax of a \created expression is as follows:

created-expression ::= \created ( spec-expression )

The argument to \created can have any reference type, and the type of the overall expression is boolean. \created(e) asserts that spec-expression e specifies an object which is created according to §12.5 and §10.3 of the JLS. This implies that e is not null.

The point at which \created changes from false to true lies within the constructor of the object. This state is therefore not visible to the created object before its constructor has finished.

The \created predicate can be used to limit a quantification over a reference type to those elements that have already been created, for instance:

(\forall Node node; \created(node); node.number <= Node.counter)

The state of \created can never change from true to false. We consider even a garbage collected object to still be created.

By the way: \fresh can be expressed in terms of \created since (\forall Object o; \fresh(o) <==> \old(\created(o)) != \created(o))