diff --git a/ArrayList/src/ArrayList.java b/ArrayList/src/ArrayList.java
index 8ffe39d..a7bbe61 100644
--- a/ArrayList/src/ArrayList.java
+++ b/ArrayList/src/ArrayList.java
@@ -82,7 +82,7 @@ private int binSearch(int v) {
 
     /*@ public normal_behaviour
       @  ensures \dl_seqPerm(\old(seq), seq);
-      @  ensures  (\forall int x,y; 0<=x<y<seq.length-1; (\bigint)seq[x] <= (\bigint)seq[y]);
+      @  ensures  (\forall int x,y; 0<=x<y<seq.length; (\bigint)seq[x] <= (\bigint)seq[y]);
       @  assignable footprint;
       @*/
     public void sort() {
diff --git a/startkey.sh b/startkey.sh
old mode 100644
new mode 100755