The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 375).

(0) Obligation:

Need to prove time_complexity of the following program:

package example_4;

public class Examples {
	
	int f = 10;

	// usual getter and setter methods
	public int getF() {
		return f;
	}

	public void setF(int f) {
		this.f = f;
	}
	
}


package example_4;

/**
 * @costaContext fields/Examples
 *
 */
public class ExamplesCont {

	Examples e;
	
	public ExamplesCont() {
		e = new Examples();
	}
}


package example_4;

/**
 * @costaContext example_4/Examples
 *
 */
public class Test {
	public void exampleMethods(ExamplesCont x, Examples y) {
		int i = 0;

		while (x.e.getF() > 0) {
			i += y.getF();
			x.e.setF(x.e.getF()-1);
		}
	}
	
	public static void main(String[] args) {
		Test o = new Test();
		ExamplesCont x = new ExamplesCont();
		Examples y = new Examples();
		o.exampleMethods(x,y);
	}
}

(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
example_4.Test.main([Ljava/lang/String;)V: Graph of 106 nodes with 1 SCC.

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) transformation)

Extracted set of 103 edges for the analysis of TIME complexity. Kept leaves.

(4) Obligation:

Set of 103 edges based on JBC Program.
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  
  • example_4.ExamplesCont: [e]
  • example_4.Examples: [f]

Considered paths: nonterm paths and paths from start to sinks

(5) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) transformation)

Extracted set of 102 edges for the analysis of TIME complexity. Dropped leaves.

(6) Obligation:

Set of 102 edges based on JBC Program.
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  
  • example_4.ExamplesCont: [e]
  • example_4.Examples: [f]

Considered paths: all paths from start

(7) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Constructed TerminationGraph.

(8) Obligation:

Termination Graph based on JBC Program:
example_4.Test.main([Ljava/lang/String;)V: Graph of 386 nodes with 0 SCCs.

(9) TerminationGraphToComplexityProof (EQUIVALENT transformation)

Proven constant complexity by absence of SCCs and edges with non-constant weight

(10) BOUNDS(CONSTANT, 375)