Termination proof of /tmp/tmp1kKSrY/RunningPointers.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 AND

    ↳5 ITRS

        ↳6 ITRStoQTRSProof (⇔)

        ↳7 QTRS

        ↳8 QTRSRRRProof (⇔)

        ↳9 QTRS

        ↳10 RisEmptyProof (⇔)

        ↳11 TRUE

    ↳12 ITRS

        ↳13 ITRStoIDPProof (⇔)

        ↳14 IDP

        ↳15 UsableRulesProof (⇔)

        ↳16 IDP

        ↳17 IDPNonInfProof (⇐)

        ↳18 IDP

        ↳19 IDependencyGraphProof (⇔)

        ↳20 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: RunningPointers

public class ObjectList {
  Object value;
  ObjectList next;

  public ObjectList(Object value, ObjectList next) {
    this.value = value;
    this.next = next;
  }

  public static ObjectList createList() {
    ObjectList result = null;
    int length = Random.random();
    while (length > 0) {
      result = new ObjectList(new Object(), result);
      length--;
    }
    return result;
  }
}


public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    String string = args[index];
    index++;
    return string.length();
  }
}


/**
 * Allegedly based on an interview question at Microsoft.
 */
public class RunningPointers {

  public static boolean isCyclic(ObjectList l) {
    if (l == null) {
      return false;
    }
    ObjectList l1, l2;
    l1 = l;
    l2 = l.next;
    while (l2 != null && l1 != l2) {
      l2 = l2.next;
      if (l2 == null) {
        return false;
      }
      else if (l2 == l1) {
        return true;
      }
      else {
        l2 = l2.next;
      }
      l1 = l1.next;
    }
    return l2 != null;
  }

  public static void main(String[] args) {
    Random.args = args;
    ObjectList list = ObjectList.createList();
    isCyclic(list);
  }
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 269 nodes with 2 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Complex Obligation (AND)

(5) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load2975(java.lang.Object(ObjectList(o2219)), java.lang.Object(ObjectList(o2219)), java.lang.Object(ObjectList(java.lang.Object(ObjectList(o2899))))) → JMP3744(java.lang.Object(ObjectList(o2219)), o2219, o2899)
JMP3744(java.lang.Object(ObjectList(o2219)), o3107, o2899) → Load2975(java.lang.Object(ObjectList(o2219)), o3107, o2899)
Load2975(java.lang.Object(ObjectList(o2219)), java.lang.Object(ObjectList(o3107)), java.lang.Object(ObjectList(java.lang.Object(ObjectList(o2899))))) → Load2975(java.lang.Object(ObjectList(o2219)), o3107, o2899)
The set Q consists of the following terms:
JMP3744(java.lang.Object(ObjectList(x0)), x1, x2)
Load2975(java.lang.Object(ObjectList(x0)), java.lang.Object(ObjectList(x1)), java.lang.Object(ObjectList(java.lang.Object(ObjectList(x2)))))

(6) ITRStoQTRSProof (EQUIVALENT transformation)

Represented integers and predefined function symbols by Terms

(7) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Load2975(java.lang.Object(ObjectList(o2219)), java.lang.Object(ObjectList(o2219)), java.lang.Object(ObjectList(java.lang.Object(ObjectList(o2899))))) → JMP3744(java.lang.Object(ObjectList(o2219)), o2219, o2899)
JMP3744(java.lang.Object(ObjectList(o2219)), o3107, o2899) → Load2975(java.lang.Object(ObjectList(o2219)), o3107, o2899)
Load2975(java.lang.Object(ObjectList(o2219)), java.lang.Object(ObjectList(o3107)), java.lang.Object(ObjectList(java.lang.Object(ObjectList(o2899))))) → Load2975(java.lang.Object(ObjectList(o2219)), o3107, o2899)

The set Q consists of the following terms:

JMP3744(java.lang.Object(ObjectList(x0)), x1, x2)
Load2975(java.lang.Object(ObjectList(x0)), java.lang.Object(ObjectList(x1)), java.lang.Object(ObjectList(java.lang.Object(ObjectList(x2)))))

(8) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(JMP3744(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(Load2975(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(ObjectList(x₁)) = 1 + x₁
POL(java.lang.Object(x₁)) = x₁

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

Load2975(java.lang.Object(ObjectList(o2219)), java.lang.Object(ObjectList(o2219)), java.lang.Object(ObjectList(java.lang.Object(ObjectList(o2899))))) → JMP3744(java.lang.Object(ObjectList(o2219)), o2219, o2899)
JMP3744(java.lang.Object(ObjectList(o2219)), o3107, o2899) → Load2975(java.lang.Object(ObjectList(o2219)), o3107, o2899)
Load2975(java.lang.Object(ObjectList(o2219)), java.lang.Object(ObjectList(o3107)), java.lang.Object(ObjectList(java.lang.Object(ObjectList(o2899))))) → Load2975(java.lang.Object(ObjectList(o2219)), o3107, o2899)

(9) Obligation:

Q restricted rewrite system:
R is empty.
The set Q consists of the following terms:

JMP3744(java.lang.Object(ObjectList(x0)), x1, x2)
Load2975(java.lang.Object(ObjectList(x0)), java.lang.Object(ObjectList(x1)), java.lang.Object(ObjectList(java.lang.Object(ObjectList(x2)))))

(10) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(11) TRUE

(12) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load876(i34) → Cond_Load876(i34 > 0, i34)
Cond_Load876(TRUE, i34) → Load876(i34 + -1)
The set Q consists of the following terms:
Load876(x0)
Cond_Load876(TRUE, x0)

(13) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
Load876(i34) → Cond_Load876(i34 > 0, i34)
Cond_Load876(TRUE, i34) → Load876(i34 + -1)

The integer pair graph contains the following rules and edges:
(0): LOAD876(i34[0]) → COND_LOAD876(i34[0] > 0, i34[0])
(1): COND_LOAD876(TRUE, i34[1]) → LOAD876(i34[1] + -1)

(0) -> (1), if ((i34[0] →^* i34[1])∧(i34[0] > 0 →^* TRUE))

(1) -> (0), if ((i34[1] + -1 →^* i34[0]))

The set Q consists of the following terms:
Load876(x0)
Cond_Load876(TRUE, x0)

(15) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(16) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD876(i34[0]) → COND_LOAD876(i34[0] > 0, i34[0])
(1): COND_LOAD876(TRUE, i34[1]) → LOAD876(i34[1] + -1)

(0) -> (1), if ((i34[0] →^* i34[1])∧(i34[0] > 0 →^* TRUE))

(1) -> (0), if ((i34[1] + -1 →^* i34[0]))

The set Q consists of the following terms:
Load876(x0)
Cond_Load876(TRUE, x0)

(17) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair LOAD876(i34) → COND_LOAD876(>(i34, 0), i34) the following chains were created:

We consider the chain LOAD876(i34[0]) → COND_LOAD876(>(i34[0], 0), i34[0]), COND_LOAD876(TRUE, i34[1]) → LOAD876(+(i34[1], -1)) which results in the following constraint:
(1)    (i34[0]=i34[1]∧>(i34[0], 0)=TRUE ⇒ LOAD876(i34[0])≥NonInfC∧LOAD876(i34[0])≥COND_LOAD876(>(i34[0], 0), i34[0])∧(U^Increasing(COND_LOAD876(>(i34[0], 0), i34[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(i34[0], 0)=TRUE ⇒ LOAD876(i34[0])≥NonInfC∧LOAD876(i34[0])≥COND_LOAD876(>(i34[0], 0), i34[0])∧(U^Increasing(COND_LOAD876(>(i34[0], 0), i34[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (i34[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_LOAD876(>(i34[0], 0), i34[0])), ≥)∧[(-1)Bound*bni_9] + [(2)bni_9]i34[0] ≥ 0∧[1 + (-1)bso_10] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (i34[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_LOAD876(>(i34[0], 0), i34[0])), ≥)∧[(-1)Bound*bni_9] + [(2)bni_9]i34[0] ≥ 0∧[1 + (-1)bso_10] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (i34[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_LOAD876(>(i34[0], 0), i34[0])), ≥)∧[(-1)Bound*bni_9] + [(2)bni_9]i34[0] ≥ 0∧[1 + (-1)bso_10] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (i34[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD876(>(i34[0], 0), i34[0])), ≥)∧[(-1)Bound*bni_9 + (2)bni_9] + [(2)bni_9]i34[0] ≥ 0∧[1 + (-1)bso_10] ≥ 0)

For Pair COND_LOAD876(TRUE, i34) → LOAD876(+(i34, -1)) the following chains were created:

We consider the chain LOAD876(i34[0]) → COND_LOAD876(>(i34[0], 0), i34[0]), COND_LOAD876(TRUE, i34[1]) → LOAD876(+(i34[1], -1)), LOAD876(i34[0]) → COND_LOAD876(>(i34[0], 0), i34[0]) which results in the following constraint:
(7)    (i34[0]=i34[1]∧>(i34[0], 0)=TRUE∧+(i34[1], -1)=i34[0]1 ⇒ COND_LOAD876(TRUE, i34[1])≥NonInfC∧COND_LOAD876(TRUE, i34[1])≥LOAD876(+(i34[1], -1))∧(U^Increasing(LOAD876(+(i34[1], -1))), ≥))

We simplified constraint (7) using rules (III), (IV) which results in the following new constraint:
(8)    (>(i34[0], 0)=TRUE ⇒ COND_LOAD876(TRUE, i34[0])≥NonInfC∧COND_LOAD876(TRUE, i34[0])≥LOAD876(+(i34[0], -1))∧(U^Increasing(LOAD876(+(i34[1], -1))), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    (i34[0] + [-1] ≥ 0 ⇒ (U^Increasing(LOAD876(+(i34[1], -1))), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [(2)bni_11]i34[0] ≥ 0∧[1 + (-1)bso_12] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (i34[0] + [-1] ≥ 0 ⇒ (U^Increasing(LOAD876(+(i34[1], -1))), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [(2)bni_11]i34[0] ≥ 0∧[1 + (-1)bso_12] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (i34[0] + [-1] ≥ 0 ⇒ (U^Increasing(LOAD876(+(i34[1], -1))), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [(2)bni_11]i34[0] ≥ 0∧[1 + (-1)bso_12] ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(12)    (i34[0] ≥ 0 ⇒ (U^Increasing(LOAD876(+(i34[1], -1))), ≥)∧[bni_11 + (-1)Bound*bni_11] + [(2)bni_11]i34[0] ≥ 0∧[1 + (-1)bso_12] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

LOAD876(i34) → COND_LOAD876(>(i34, 0), i34)
- (i34[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD876(>(i34[0], 0), i34[0])), ≥)∧[(-1)Bound*bni_9 + (2)bni_9] + [(2)bni_9]i34[0] ≥ 0∧[1 + (-1)bso_10] ≥ 0)
COND_LOAD876(TRUE, i34) → LOAD876(+(i34, -1))
- (i34[0] ≥ 0 ⇒ (U^Increasing(LOAD876(+(i34[1], -1))), ≥)∧[bni_11 + (-1)Bound*bni_11] + [(2)bni_11]i34[0] ≥ 0∧[1 + (-1)bso_12] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD876(x₁)) = [2]x₁
POL(COND_LOAD876(x₁, x₂)) = [-1] + [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]

The following pairs are in P_>:

LOAD876(i34[0]) → COND_LOAD876(>(i34[0], 0), i34[0])
COND_LOAD876(TRUE, i34[1]) → LOAD876(+(i34[1], -1))

The following pairs are in P_bound:

LOAD876(i34[0]) → COND_LOAD876(>(i34[0], 0), i34[0])
COND_LOAD876(TRUE, i34[1]) → LOAD876(+(i34[1], -1))

The following pairs are in P_≥:
none

There are no usable rules.

(18) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:
Load876(x0)
Cond_Load876(TRUE, x0)

(19) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

(0) Obligation:

(1) JBC2FIG (SOUND transformation)

(2) Obligation:

(3) FIGtoITRSProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) ITRStoQTRSProof (EQUIVALENT transformation)

(7) Obligation:

(8) QTRSRRRProof (EQUIVALENT transformation)

(9) Obligation:

(10) RisEmptyProof (EQUIVALENT transformation)

(11) TRUE

(12) Obligation:

(13) ITRStoIDPProof (EQUIVALENT transformation)

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) IDPNonInfProof (SOUND transformation)

(18) Obligation:

(19) IDependencyGraphProof (EQUIVALENT transformation)

(20) TRUE