Invariants do not work with private inner class

[nhatminhle]

From depri...@broadinstitute.org on May 19, 2011 19:18:13

What steps will reproduce the problem? 1. Create a private final class, annotate it with @Invariants, and compilation of the contracts fails

public class GenomeLocParser { private static Logger logger = Logger.getLogger(GenomeLocParser.class); private final MasterSequenceDictionary contigInfo;

@Invariant({
        "dict != null",
        "dict.size() > 0",
        "lastSSR == null || dict.getSequence(lastContig).getSequenceIndex() == lastIndex",
        "lastSSR == null || dict.getSequence(lastContig) == lastContig",
        "lastSSR == null || dict.getSequence(lastContig) == lastSRR"})
private final class MasterSequenceDictionary {
    final private SAMSequenceDictionary dict;
    SAMSequenceRecord lastSSR = null;
    String lastContig = "";
    int lastIndex = -1;

et cetera }

When you compile this, the cofoja annotations are failing with errors like symbol not found: lastSSR. What version of the product are you using? On what operating system? r120

Original issue: http://code.google.com/p/cofoja/issues/detail?id=21

[nhatminhle]

From nhat.min...@gmail.com on May 20, 2011 00:47:40

Hum, lastConfig is a String that you're comparing to a SAMSequenceRecord. And you wrote "SRR" instead of "SSR", hence symbol not found; aside from that, compiles fine for me.

[nhatminhle]

From depri...@broadinstitute.org on May 20, 2011 08:19:52

Yes, sorry about that. I got it working right away. I've discovered a separate issue, which I'll post in a separate thread.

[nhatminhle]

From nhat.min...@gmail.com on May 20, 2011 08:33:10

Status: Invalid