Proving createdness of sequence elements

[FliegendeWurst]

Description

I would like to be able to prove ==> (ClassName)seq[i_0].<created> = TRUE, where I already know ==> (ClassName)seq[i_0] = null.

My current solution is to add a new taclet:

referencedObjectIsCreatedRightSeqGet {
    \schemaVar \term Heap h;
    \schemaVar \term Seq s1;
    \schemaVar \term int iv;

    \assumes( ==> alpha::seqGet(s1, iv) = null)
    \find( ==> boolean::select(h,
            alpha::seqGet(s1, iv),
            java.lang.Object::<created>) = TRUE)

    \replacewith( ==> wellFormed(h))

    \heuristics(concrete)
};

with type definitions

\sorts {
    \generic alpha \extends java.lang.Object;
}

But @WolframPfeifer pointed out that sequence elements are not necessarily created objects.

[wadoon]

I am not sure, what the intention of this issue is.

Of course, @WolframPfeifer is right. Within sequence, you put anything, also things that are not an object at all (ints, locsets, ...).

For me, this is a classical constraint that you put in your invariant. On the other side, I am not sure whether the field <created> is accessible via JML.