Crash

[pys]

/Users/pys/src/openjml-macos-arm64-21.0.26/openjml -Xlint:unchecked /Users/pys/src/IdeaProjects/jun26/src/ArrayQueue.java
/Users/pys/src/IdeaProjects/jun26/src/ArrayQueue.java:1: error: ArrayQueue is not abstract and does not override abstract method peek() in BoundedQueue
public class ArrayQueue implements BoundedQueue {
^
where E is a type-variable:
E extends Object declared in class ArrayQueue
/Users/pys/src/IdeaProjects/jun26/src/ArrayQueue.java:10: error: Because 'max' reads 'a' in a represents clause, 'a' must be 'in' the model field 'max'
private represents max = a.length;
^
/Users/pys/src/IdeaProjects/jun26/src/ArrayQueue.java:11: error: Because 'q' reads 'size' in a represents clause, 'size' must be 'in' the model field 'q'
private represents q = (size == 0) ? \seq.empty()
^
/Users/pys/src/IdeaProjects/jun26/src/ArrayQueue.java:12: error: Because 'q' reads 'head' in a represents clause, 'head' must be 'in' the model field 'q'
: (head < last) ? a[head..last-1]
^
/Users/pys/src/IdeaProjects/jun26/src/ArrayQueue.java:12: error: Because 'q' reads 'last' in a represents clause, 'last' must be 'in' the model field 'q'
: (head < last) ? a[head..last-1]
^
./BoundedQueue.java:36: warning: [unchecked] unchecked generic array creation for varargs parameter of type E[]
@ ensures q == \old(q)+\seq.of(o);
^
where E is a type-variable:
E extends Object declared in interface BoundedQueue
5 errors
1 warning
java.lang.AssertionError
at jdk.compiler/com.sun.tools.javac.util.Assert.error(Assert.java:155)
at jdk.compiler/com.sun.tools.javac.tree.TreeScanner.visitTree(TreeScanner.java:421)
at jdk.compiler/com.sun.tools.javac.comp.DeferredAttr$DeferredAttrDiagHandler$PosScanner.visitTree(DeferredAttr.java:600)
at jdk.compiler/org.jmlspecs.openjml.JmlTree$JmlRange.accept(JmlTree.java:3058)
at jdk.compiler/com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:50)
at jdk.compiler/com.sun.tools.javac.comp.DeferredAttr$DeferredAttrDiagHandler$PosScanner.scan(DeferredAttr.java:593)
at jdk.compiler/com.sun.tools.javac.tree.TreeScanner.visitIndexed(TreeScanner.java:339)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCArrayAccess.accept(JCTree.java:2547)
at jdk.compiler/com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:50)
at jdk.compiler/com.sun.tools.javac.comp.DeferredAttr$DeferredAttrDiagHandler$PosScanner.scan(DeferredAttr.java:593)
at jdk.compiler/com.sun.tools.javac.comp.DeferredAttr$DeferredAttrDiagHandler.lambda$new$0(DeferredAttr.java:607)
at jdk.compiler/com.sun.tools.javac.util.Log$DeferredDiagnosticHandler.report(Log.java:151)
at jdk.compiler/com.sun.tools.javac.util.Log.report(Log.java:674)
at jdk.compiler/com.sun.tools.javac.util.AbstractLog.error(AbstractLog.java:126)
at jdk.compiler/org.jmlspecs.openjml.Utils.error(Utils.java:1818)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.visitIdent(JmlAttr.java:6153)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCIdent.accept(JCTree.java:2715)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attribTree(Attr.java:664)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attribTree(JmlAttr.java:5099)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attribExpr(Attr.java:718)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.visitIndexed(JmlAttr.java:6286)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCArrayAccess.accept(JCTree.java:2547)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attribTree(Attr.java:664)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attribTree(JmlAttr.java:5099)
at jdk.compiler/com.sun.tools.javac.comp.DeferredAttr.attribSpeculative(DeferredAttr.java:563)
at jdk.compiler/com.sun.tools.javac.comp.DeferredAttr.attribSpeculative(DeferredAttr.java:543)
at jdk.compiler/com.sun.tools.javac.comp.DeferredAttr.attribSpeculative(DeferredAttr.java:535)
at jdk.compiler/com.sun.tools.javac.comp.Attr.isBooleanOrNumeric(Attr.java:2128)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.isBooleanOrNumeric(JmlAttr.java:8629)
at jdk.compiler/com.sun.tools.javac.comp.Attr.isBooleanOrNumeric(Attr.java:2106)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.isBooleanOrNumeric(JmlAttr.java:8629)
at jdk.compiler/com.sun.tools.javac.comp.Attr.visitConditional(Attr.java:2044)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.visitConditional(JmlAttr.java:5126)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCConditional.accept(JCTree.java:1536)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attribTree(Attr.java:664)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attribTree(JmlAttr.java:5099)
at jdk.compiler/com.sun.tools.javac.comp.Attr.visitConditional(Attr.java:2076)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.visitConditional(JmlAttr.java:5126)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCConditional.accept(JCTree.java:1536)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attribTree(Attr.java:664)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attribTree(JmlAttr.java:5099)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attribExpr(Attr.java:711)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attribExpr(JmlAttr.java:8292)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.visitJmlTypeClauseRepresents(JmlAttr.java:3875)
at jdk.compiler/org.jmlspecs.openjml.JmlTree$JmlTypeClauseRepresents.accept(JmlTree.java:4208)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attribTree(Attr.java:664)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attribTree(JmlAttr.java:5099)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attrTypeClause(JmlAttr.java:8903)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attrSpecs(JmlAttr.java:8954)
at jdk.compiler/org.jmlspecs.openjml.JmlSpecs.getAttrSpecs(JmlSpecs.java:697)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attrSpecs(JmlAttr.java:8755)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attribMethodSpecsAndBody(JmlAttr.java:1573)
at jdk.compiler/com.sun.tools.javac.comp.Attr.visitMethodDef(Attr.java:1234)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.visitMethodDef(JmlAttr.java:1435)
at jdk.compiler/org.jmlspecs.openjml.JmlTree$JmlMethodDecl.accept(JmlTree.java:1432)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attribTree(Attr.java:664)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attribTree(JmlAttr.java:5099)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attribStat(Attr.java:739)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attribStat(JmlAttr.java:598)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attribClassBody(Attr.java:5698)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attribClassBody(JmlAttr.java:574)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attribClass(Attr.java:5585)
at jdk.compiler/com.sun.tools.javac.comp.JmlAttr.attribClass(JmlAttr.java:455)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attribClass(Attr.java:5404)
at jdk.compiler/com.sun.tools.javac.comp.Attr.attrib(Attr.java:5343)
at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.attribute(JavaCompiler.java:1364)
at jdk.compiler/com.sun.tools.javac.main.JmlCompiler.attribute(JmlCompiler.java:587)
at jdk.compiler/com.sun.tools.javac.main.JmlCompiler.attribute(JmlCompiler.java:545)
at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:971)
at jdk.compiler/com.sun.tools.javac.main.JmlCompiler.compile(JmlCompiler.java:211)
at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:337)
at jdk.compiler/org.jmlspecs.openjml.Main.compile(Main.java:470)
at jdk.compiler/org.jmlspecs.openjml.Main.execute(Main.java:296)
at jdk.compiler/org.jmlspecs.openjml.Main.execute(Main.java:253)
at jdk.compiler/org.jmlspecs.openjml.Main.main(Main.java:218)
at jdk.compiler/com.sun.tools.javac.Main.main(Main.java:53)
error: A catastrophic JML internal error occurred. Please report the bug with as much information as you can.
Reason: Unexpected Throwable error caught. Use STACK= to see the stack trace

[davidcok]

Thanks for the report. Can you share the relevant source code?

[pys]

Oops I thought I did. Second trial, in the meantime my source changed a bit but it stills gives the same error. Clearly the culprit is the ‘represents q’ clause:

represents q = (size == 0) ? \seq.empty()
: (head < last) ? \seq.of(a[head..last-1])
: \seq.of(a[head..a.length-1])+\seq.of(a[0..last-1]);

[davidcok]

Still no source code. A zip file will do.

[pys]

Attachments do not work?
I copy-paste it below :
—
public class ArrayQueue implements BoundedQueue {
// Bounded queue implemented as a rotating array.
private E[] a; //@ in max, q; // contains the queue between head (included) and last (excluded)
private int head; //@ in q;
private int last; //@ in q;
private int size; //@ in q;
/@ private invariant a != null;
private invariant 0 <= size <= a.length; // number of elements in the queue
private invariant 0 <= head < a.length; // index of the first element (if any)
private invariant 0 <= last < a.length; // index of the future last element, not yet in the queue
private invariant (head+size) % a.length == last;
private represents max = a.length;
private represents q = (size == 0) ? \seq.empty()
: (head < last) ? \seq.of(a[head..last-1])
: \seq.of(a[head..a.length-1])+\seq.of(a[0..last-1]);
@/

/*@ requires m > 0;
 @ ensures q == \seq.<E>empty();
 @ ensures max == m;
 @ pure
 @*/
public ArrayQueue(int m) {
    E[] a = new E[m];
    head = last = size = 0;
}

public boolean isEmpty() {
    return size == 0;
}

public int size() {
    return size;
}

public int capacity() {
    return a.length;
}

//@ ensures \result <==> size() == capacity();
public boolean isFull() {
    return size == a.length;
}

public boolean add(E x) {
    if (!isFull()) {
        size++;
        a[last] = x;
        last = (last++) % a.length;
        return true; // has been added
    } else throw new IllegalStateException("Queue is full");
}

public E remove() {
    if (!isEmpty()) {
        size--;
        E result = a[head];
        head = (head++) % a.length;
        return result;  // can be null (when containsNull is true)
    }
    return null;
}

public E peek() {
    if (!isEmpty())
        return a[head]; // can be null (when containsNull is true)
    else return null;
}

}

[davidcok]

Thanks for ArrayQueue, but I do need all the source code so I can reproduce the problem. At present I'm missing BoundedQueue and any dependencies it might have.

[pys]

I see the generic type has been garbled by GitHub.

[pys]

BoundedQueue (with generic type garbled by Github I guess) :
—
import java.util.*;

public interface BoundedQueue {

// similar to java.util.Queue but specified as bounded
//@ model public instance \seq<E> q; // in JML version < 2, use JMLObjectSequence
//@ model public instance int max; // The capacity (maximal size) of the queue, fixed at creation
//@ public constraint max == \old(max);
//@ public invariant size() <= max;

/* requires m > 0;
  @ ensures q == \seq.<E>empty();
 @ ensures max == m;
 @ pure
  BoundedQueue<E>(int m);  //creates an empty queue of capacity m
 Constructors are forbidden in Java interfaces.
 */

// current number of items in the queue
//@ ensures \result == q.length();
//@ strictly_pure
int size();

//@ ensures \result == max;
//@ pure
int capacity();

//@ ensures \result == (size() == 0);
//@ strictly_pure
boolean isEmpty();

// according to the Java description of a queue, 'add' will return true if element o is really added,
// but will never return false and instead raise IllegalStateException when it fails.
/*@ requires size() < max;
@ ensures size() == \old(size()) + 1;
@ ensures  q == \old(q)+\seq.<E>of(o);
@ ensures \result;  // returns true
@ assignable q;
@ also
@ exceptional_behaviour
@ requires size() == max;    //full
@ assignable \nothing;
@ signals (IllegalStateException e);
 @*/
boolean add(E o);

// Returns and removes the head of the queue.
/*@  normal_behavior
  @   requires !isEmpty();
  @   assignable q;
  @   ensures \result == \old(q[0]);
  @   ensures (\forall int i; 0 < i < q.length; q[i-1] == \old(q[i]));
  @   ensures size() == \old(size()) -1;
@ also
@ exceptional_behaviour
@ requires size() == 0;
@   assignable \nothing;
@ signals (NoSuchElementException e);
 @*/
E remove();

// Returns the head of the queue, or null if empty.
/*@ normal_behavior
  @   requires !isEmpty();
  @   ensures \result == q[0];
 @ also
 @ normal_behavior
 @ requires isEmpty();
 @   ensures \result == null;
 @ pure
  @*/
E peek();

}