{
"evaluationState" : {
"id" : "aa43bc30-c679-4df3-9710-deeb1ffa2a5d",
"startTime" : "2026-09-08T05:35:57.47239Z",
"endTime" : "2026-09-08T05:37:57.623722Z",
"status" : "SUCCESS",
"commitHash" : "fec846914ad97ffc3fb456d7c975e1387aba2364"
},
"stepResults" : {
"structure" : {
"name" : "main",
"similarityToProf" : 0.4999934747551029,
"codeComplexity" : 0.4995812539950448,
"programmingTime" : 0.499997957065592,
"codeUnderstandability" : 0.5005583280066069,
"children" : [ {
"name" : "ch.fhnw.autofeedback",
"similarityToProf" : 0.4999934747551029,
"codeComplexity" : 0.4995812539950448,
"programmingTime" : 0.499997957065592,
"codeUnderstandability" : 0.5005583280066069,
"children" : [ {
"name" : "ExampleProblemImpl",
"similarityToProf" : 0.5,
"codeComplexity" : 0.5,
"programmingTime" : 0.5,
"codeUnderstandability" : 0.5,
"children" : [ {
"name" : "public int max(int a, int b)",
"similarityToProf" : 0.5,
"codeComplexity" : 0.5,
"programmingTime" : 0.5,
"codeUnderstandability" : 0.5,
"children" : [ ]
} ]
}, {
"name" : "ForLoop",
"similarityToProf" : 0.4942546220879088,
"codeComplexity" : 0.4852297668200001,
"programmingTime" : 0.4921561132665877,
"codeUnderstandability" : 0.51969364424,
"children" : [ {
"name" : " int forloop(int x)",
"similarityToProf" : 0.4942546220879088,
"codeComplexity" : 0.4852297668200001,
"programmingTime" : 0.4921561132665877,
"codeUnderstandability" : 0.51969364424,
"children" : [ ]
} ]
}, {
"name" : "MergeSort",
"similarityToProf" : 0.5,
"codeComplexity" : 0.5,
"programmingTime" : 0.5,
"codeUnderstandability" : 0.5,
"children" : [ {
"name" : "private void merge(int[] arr, int low, int mid, int high)",
"similarityToProf" : 0.5,
"codeComplexity" : 0.5,
"programmingTime" : 0.5,
"codeUnderstandability" : 0.5,
"children" : [ ]
}, {
"name" : "public void sort(int[] arr, int low, int high)",
"similarityToProf" : 0.5,
"codeComplexity" : 0.5,
"programmingTime" : 0.5,
"codeUnderstandability" : 0.5,
"children" : [ ]
} ]
} ]
} ]
},
"verification" : {
"resultsPerFile" : {
"ForLoop.java" : {
"isValid" : false,
"results" : [ {
"methodName" : "ch.fhnw.autofeedback.ForLoop.ForLoop()",
"isValid" : true,
"status" : [ {
"file" : "/work/ForLoop.java",
"line" : 3,
"check" : "Feasibility check #1 - after static initialization ",
"result" : " OK [0.01 secs]"
}, {
"file" : "/work/ForLoop.java",
"line" : 3,
"check" : "Feasibility check #2 - after static initial state assumption ",
"result" : " OK [0.00 secs]"
}, {
"file" : "/work/ForLoop.java",
"line" : 3,
"check" : "Feasibility check #3 - after inherited fields ",
"result" : " OK [0.00 secs]"
}, {
"file" : "/work/ForLoop.java",
"line" : 3,
"check" : "Feasibility check #4 - after allocation assumption ",
"result" : " OK [0.00 secs]"
}, {
"file" : "/work/ForLoop.java",
"line" : 3,
"check" : "Feasibility check #5 - after invariants for receiver of ForLoop() ",
"result" : " OK [0.00 secs]"
}, {
"file" : "/work/ForLoop.java",
"line" : 3,
"check" : "Feasibility check #6 - end of preconditions ",
"result" : " OK [0.00 secs]"
}, {
"file" : "/work/ForLoop.java",
"line" : 3,
"check" : "Feasibility check #7 - before call ",
"result" : " OK [0.00 secs]"
}, {
"file" : "/work/ForLoop.java",
"line" : 3,
"check" : "Feasibility check #8 - after call ",
"result" : " OK [0.00 secs]"
}, {
"file" : "/work/ForLoop.java",
"line" : 1,
"check" : "Feasibility check #9 - at implicit return ",
"result" : " OK [0.00 secs]"
}, {
"file" : "/work/ForLoop.java",
"line" : 1,
"check" : "Feasibility check #10 - at program exit ",
"result" : " OK [0.00 secs]"
} ],
"warnings" : [ ],
"endLineNr" : 14,
"feedback" : "Feasibility check #1 - after static initialization OK [0.01 secs]\nFeasibility check #2 - after static initial state assumption OK [0.00 secs]\nFeasibility check #3 - after inherited fields OK [0.00 secs]\nFeasibility check #4 - after allocation assumption OK [0.00 secs]\nFeasibility check #5 - after invariants for receiver of ForLoop() OK [0.00 secs]\nFeasibility check #6 - end of preconditions OK [0.00 secs]\nFeasibility check #7 - before call OK [0.00 secs]\nFeasibility check #8 - after call OK [0.00 secs]\nFeasibility check #9 - at implicit return OK [0.00 secs]\nFeasibility check #10 - at program exit OK [0.00 secs]\n"
}, {
"methodName" : "ch.fhnw.autofeedback.ForLoop.forloop(int)",
"isValid" : false,
"status" : [ ],
"warnings" : [ {
"endLineNr" : 141,
"warning" : "/work/ForLoop.java:22: verify The prover cannot establish an assertion (Postcondition /work/ForLoop.java:6:) in method forloop\n return x;\n ^\n/work/ForLoop.java:6: verify Associated declaration /work/ForLoop.java:22:\n ensures \\result == 0;\n ^\n",
"trace" : "/work/ForLoop.java:1: \trequires true; \n\t\t\tVALUE true\t === true\n/work/ForLoop.java:5: \trequires x == -15; \n\t\t\tVALUE x\t === ( - 15 )\n\t\t\tVALUE -15\t === ( - 15 )\n\t\t\tVALUE x == -15\t === true\n/work/ForLoop.java:10: \tint i = 1\n\t\t\tVALUE 1\t === 1\n\t\t\tVALUE i\t === 1\n/work/ForLoop.java:11: \tx += 2\n\t\t\tVALUE 2\t === 2\n\t\t\tVALUE x += 2\t === ( - 13 )\n/work/ForLoop.java:11: \tArithmeticOperationRange assertion _JML__tmp`12 || (!(0 < _JML__tmp`10 && 0 < 2) || _JML__tmp`10 <= 2147483647 - 2)\n\t\t\tVALUE !(0 < _JML__tmp`10 && 0 < 2) || _JML__tmp`10 <= 2147483647 - 2\t === true\n/work/ForLoop.java:11: \tArithmeticOperationRange assertion _JML__tmp`14 || (!(_JML__tmp`10 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`10)\n\t\t\tVALUE !(_JML__tmp`10 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`10\t === true\n/work/ForLoop.java:12: \ti++\n\t\t\tVALUE i\t === 1\n\t\t\tVALUE i++\t === 1\n/work/ForLoop.java:12: \tArithmeticOperationRange assertion _JML__tmp`22 || (!(0 < _JML__tmp`20 && 0 < 1) || _JML__tmp`20 <= 2147483647 - 1)\n\t\t\tVALUE !(0 < _JML__tmp`20 && 0 < 1) || _JML__tmp`20 <= 2147483647 - 1\t === true\n/work/ForLoop.java:12: \tArithmeticOperationRange assertion _JML__tmp`24 || (!(_JML__tmp`20 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`20)\n\t\t\tVALUE !(_JML__tmp`20 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`20\t === true\n/work/ForLoop.java:13: \tx += 2\n\t\t\tVALUE 2\t === 2\n\t\t\tVALUE x += 2\t === ( - 11 )\n/work/ForLoop.java:13: \tArithmeticOperationRange assertion _JML__tmp`31 || (!(0 < _JML__tmp`29 && 0 < 2) || _JML__tmp`29 <= 2147483647 - 2)\n\t\t\tVALUE !(0 < _JML__tmp`29 && 0 < 2) || _JML__tmp`29 <= 2147483647 - 2\t === true\n/work/ForLoop.java:13: \tArithmeticOperationRange assertion _JML__tmp`33 || (!(_JML__tmp`29 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`29)\n\t\t\tVALUE !(_JML__tmp`29 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`29\t === true\n/work/ForLoop.java:14: \ti++\n\t\t\tVALUE i\t === 2\n\t\t\tVALUE i++\t === 2\n/work/ForLoop.java:14: \tArithmeticOperationRange assertion _JML__tmp`41 || (!(0 < _JML__tmp`39 && 0 < 1) || _JML__tmp`39 <= 2147483647 - 1)\n\t\t\tVALUE !(0 < _JML__tmp`39 && 0 < 1) || _JML__tmp`39 <= 2147483647 - 1\t === true\n/work/ForLoop.java:14: \tArithmeticOperationRange assertion _JML__tmp`43 || (!(_JML__tmp`39 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`39)\n\t\t\tVALUE !(_JML__tmp`39 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`39\t === true\n/work/ForLoop.java:15: \tx += 2\n\t\t\tVALUE 2\t === 2\n\t\t\tVALUE x += 2\t === ( - 9 )\n/work/ForLoop.java:15: \tArithmeticOperationRange assertion _JML__tmp`50 || (!(0 < _JML__tmp`48 && 0 < 2) || _JML__tmp`48 <= 2147483647 - 2)\n\t\t\tVALUE !(0 < _JML__tmp`48 && 0 < 2) || _JML__tmp`48 <= 2147483647 - 2\t === true\n/work/ForLoop.java:15: \tArithmeticOperationRange assertion _JML__tmp`52 || (!(_JML__tmp`48 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`48)\n\t\t\tVALUE !(_JML__tmp`48 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`48\t === true\n/work/ForLoop.java:16: \ti++\n\t\t\tVALUE i\t === 3\n\t\t\tVALUE i++\t === 3\n/work/ForLoop.java:16: \tArithmeticOperationRange assertion _JML__tmp`60 || (!(0 < _JML__tmp`58 && 0 < 1) || _JML__tmp`58 <= 2147483647 - 1)\n\t\t\tVALUE !(0 < _JML__tmp`58 && 0 < 1) || _JML__tmp`58 <= 2147483647 - 1\t === true\n/work/ForLoop.java:16: \tArithmeticOperationRange assertion _JML__tmp`62 || (!(_JML__tmp`58 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`58)\n\t\t\tVALUE !(_JML__tmp`58 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`58\t === true\n/work/ForLoop.java:17: \tx += 2\n\t\t\tVALUE 2\t === 2\n\t\t\tVALUE x += 2\t === ( - 7 )\n/work/ForLoop.java:17: \tArithmeticOperationRange assertion _JML__tmp`69 || (!(0 < _JML__tmp`67 && 0 < 2) || _JML__tmp`67 <= 2147483647 - 2)\n\t\t\tVALUE !(0 < _JML__tmp`67 && 0 < 2) || _JML__tmp`67 <= 2147483647 - 2\t === true\n/work/ForLoop.java:17: \tArithmeticOperationRange assertion _JML__tmp`71 || (!(_JML__tmp`67 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`67)\n\t\t\tVALUE !(_JML__tmp`67 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`67\t === true\n/work/ForLoop.java:18: \ti++\n\t\t\tVALUE i\t === 4\n\t\t\tVALUE i++\t === 4\n/work/ForLoop.java:18: \tArithmeticOperationRange assertion _JML__tmp`79 || (!(0 < _JML__tmp`77 && 0 < 1) || _JML__tmp`77 <= 2147483647 - 1)\n\t\t\tVALUE !(0 < _JML__tmp`77 && 0 < 1) || _JML__tmp`77 <= 2147483647 - 1\t === true\n/work/ForLoop.java:18: \tArithmeticOperationRange assertion _JML__tmp`81 || (!(_JML__tmp`77 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`77)\n\t\t\tVALUE !(_JML__tmp`77 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`77\t === true\n/work/ForLoop.java:19: \tx += 2\n\t\t\tVALUE 2\t === 2\n\t\t\tVALUE x += 2\t === ( - 5 )\n/work/ForLoop.java:19: \tArithmeticOperationRange assertion _JML__tmp`88 || (!(0 < _JML__tmp`86 && 0 < 2) || _JML__tmp`86 <= 2147483647 - 2)\n\t\t\tVALUE !(0 < _JML__tmp`86 && 0 < 2) || _JML__tmp`86 <= 2147483647 - 2\t === true\n/work/ForLoop.java:19: \tArithmeticOperationRange assertion _JML__tmp`90 || (!(_JML__tmp`86 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`86)\n\t\t\tVALUE !(_JML__tmp`86 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`86\t === true\n/work/ForLoop.java:20: \ti++\n\t\t\tVALUE i\t === 5\n\t\t\tVALUE i++\t === 5\n/work/ForLoop.java:20: \tArithmeticOperationRange assertion _JML__tmp`98 || (!(0 < _JML__tmp`96 && 0 < 1) || _JML__tmp`96 <= 2147483647 - 1)\n\t\t\tVALUE !(0 < _JML__tmp`96 && 0 < 1) || _JML__tmp`96 <= 2147483647 - 1\t === true\n/work/ForLoop.java:20: \tArithmeticOperationRange assertion _JML__tmp`100 || (!(_JML__tmp`96 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`96)\n\t\t\tVALUE !(_JML__tmp`96 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`96\t === true\n/work/ForLoop.java:22: \treturn x;\n/work/ForLoop.java:6: \tensures \\result == 0; \n\t\t\tVALUE \\result\t === ( - 5 )\n\t\t\tVALUE 0\t === 0\n\t\t\tVALUE \\result == 0\t === false\n/work/ForLoop.java:22: Invalid assertion (Postcondition)\n /work/ForLoop.java:6: Associated location\n",
"counterexample" : "java.lang.Object_theHashCode_2969_0___2 = ( ( as const ( Array REF Int ) ) ( - 2147462410 ) )\n`THIS = |`THIS|\njava.lang.Object_`alloc___38_0___4 = ( store ( ( as const ( Array REF Int ) ) 0 ) REF!val!6 ( - 7719 ) )\n`THIS = |`THIS|\nASSERT_29_127 = true\nASSERT_43_127 = true\n__JML_FeasCheck_ = 0\nASSERT_47_127 = true\n`result_127_127___11 = 0\ni_170_170___13 = 0\nASSERT_41_127 = true\nASSERT_33_127 = true\n`exception_127_127___8 = NULL\nASSERT_38_127 = true\nASSERT_45_127 = true\nx_0_0___7 = 0\nASSERT_32_127 = true\njava.lang.Object_`isalloc___38_0___5 = ( ( as const ( Array REF Bool ) ) true )\nASSERT_40_127 = true\nPre_2_74_63___14 = true\nASSERT_39_127 = true\nx_139_139___10 = ( - 15 )\n_JML__tmp`6 = true\njava.lang.Object___owner_2072_0___6 = ( ( as const ( Array REF REF ) ) REF!val!6 )\n_JML__tmp`7 = true\nch.fhnw.autofeedback.ForLoop__heap___0_127___12 = 2\n`terminationPosition_127_127___9 = 0\n"
} ],
"endLineNr" : 142,
"feedback" : "Attention the line numbers are calculated and could be wrong!\n/work/ForLoop.java:22: verify The prover cannot establish an assertion (Postcondition /work/ForLoop.java:6:) in method forloop\n return x;\n ^\n/work/ForLoop.java:6: verify Associated declaration /work/ForLoop.java:22:\n ensures \\result == 0;\n ^\n%%TRACE%%/work/ForLoop.java:1: \trequires true; \n\t\t\tVALUE true\t === true\n/work/ForLoop.java:5: \trequires x == -15; \n\t\t\tVALUE x\t === ( - 15 )\n\t\t\tVALUE -15\t === ( - 15 )\n\t\t\tVALUE x == -15\t === true\n/work/ForLoop.java:10: \tint i = 1\n\t\t\tVALUE 1\t === 1\n\t\t\tVALUE i\t === 1\n/work/ForLoop.java:11: \tx += 2\n\t\t\tVALUE 2\t === 2\n\t\t\tVALUE x += 2\t === ( - 13 )\n/work/ForLoop.java:11: \tArithmeticOperationRange assertion _JML__tmp`12 || (!(0 < _JML__tmp`10 && 0 < 2) || _JML__tmp`10 <= 2147483647 - 2)\n\t\t\tVALUE !(0 < _JML__tmp`10 && 0 < 2) || _JML__tmp`10 <= 2147483647 - 2\t === true\n/work/ForLoop.java:11: \tArithmeticOperationRange assertion _JML__tmp`14 || (!(_JML__tmp`10 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`10)\n\t\t\tVALUE !(_JML__tmp`10 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`10\t === true\n/work/ForLoop.java:12: \ti++\n\t\t\tVALUE i\t === 1\n\t\t\tVALUE i++\t === 1\n/work/ForLoop.java:12: \tArithmeticOperationRange assertion _JML__tmp`22 || (!(0 < _JML__tmp`20 && 0 < 1) || _JML__tmp`20 <= 2147483647 - 1)\n\t\t\tVALUE !(0 < _JML__tmp`20 && 0 < 1) || _JML__tmp`20 <= 2147483647 - 1\t === true\n/work/ForLoop.java:12: \tArithmeticOperationRange assertion _JML__tmp`24 || (!(_JML__tmp`20 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`20)\n\t\t\tVALUE !(_JML__tmp`20 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`20\t === true\n/work/ForLoop.java:13: \tx += 2\n\t\t\tVALUE 2\t === 2\n\t\t\tVALUE x += 2\t === ( - 11 )\n/work/ForLoop.java:13: \tArithmeticOperationRange assertion _JML__tmp`31 || (!(0 < _JML__tmp`29 && 0 < 2) || _JML__tmp`29 <= 2147483647 - 2)\n\t\t\tVALUE !(0 < _JML__tmp`29 && 0 < 2) || _JML__tmp`29 <= 2147483647 - 2\t === true\n/work/ForLoop.java:13: \tArithmeticOperationRange assertion _JML__tmp`33 || (!(_JML__tmp`29 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`29)\n\t\t\tVALUE !(_JML__tmp`29 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`29\t === true\n/work/ForLoop.java:14: \ti++\n\t\t\tVALUE i\t === 2\n\t\t\tVALUE i++\t === 2\n/work/ForLoop.java:14: \tArithmeticOperationRange assertion _JML__tmp`41 || (!(0 < _JML__tmp`39 && 0 < 1) || _JML__tmp`39 <= 2147483647 - 1)\n\t\t\tVALUE !(0 < _JML__tmp`39 && 0 < 1) || _JML__tmp`39 <= 2147483647 - 1\t === true\n/work/ForLoop.java:14: \tArithmeticOperationRange assertion _JML__tmp`43 || (!(_JML__tmp`39 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`39)\n\t\t\tVALUE !(_JML__tmp`39 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`39\t === true\n/work/ForLoop.java:15: \tx += 2\n\t\t\tVALUE 2\t === 2\n\t\t\tVALUE x += 2\t === ( - 9 )\n/work/ForLoop.java:15: \tArithmeticOperationRange assertion _JML__tmp`50 || (!(0 < _JML__tmp`48 && 0 < 2) || _JML__tmp`48 <= 2147483647 - 2)\n\t\t\tVALUE !(0 < _JML__tmp`48 && 0 < 2) || _JML__tmp`48 <= 2147483647 - 2\t === true\n/work/ForLoop.java:15: \tArithmeticOperationRange assertion _JML__tmp`52 || (!(_JML__tmp`48 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`48)\n\t\t\tVALUE !(_JML__tmp`48 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`48\t === true\n/work/ForLoop.java:16: \ti++\n\t\t\tVALUE i\t === 3\n\t\t\tVALUE i++\t === 3\n/work/ForLoop.java:16: \tArithmeticOperationRange assertion _JML__tmp`60 || (!(0 < _JML__tmp`58 && 0 < 1) || _JML__tmp`58 <= 2147483647 - 1)\n\t\t\tVALUE !(0 < _JML__tmp`58 && 0 < 1) || _JML__tmp`58 <= 2147483647 - 1\t === true\n/work/ForLoop.java:16: \tArithmeticOperationRange assertion _JML__tmp`62 || (!(_JML__tmp`58 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`58)\n\t\t\tVALUE !(_JML__tmp`58 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`58\t === true\n/work/ForLoop.java:17: \tx += 2\n\t\t\tVALUE 2\t === 2\n\t\t\tVALUE x += 2\t === ( - 7 )\n/work/ForLoop.java:17: \tArithmeticOperationRange assertion _JML__tmp`69 || (!(0 < _JML__tmp`67 && 0 < 2) || _JML__tmp`67 <= 2147483647 - 2)\n\t\t\tVALUE !(0 < _JML__tmp`67 && 0 < 2) || _JML__tmp`67 <= 2147483647 - 2\t === true\n/work/ForLoop.java:17: \tArithmeticOperationRange assertion _JML__tmp`71 || (!(_JML__tmp`67 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`67)\n\t\t\tVALUE !(_JML__tmp`67 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`67\t === true\n/work/ForLoop.java:18: \ti++\n\t\t\tVALUE i\t === 4\n\t\t\tVALUE i++\t === 4\n/work/ForLoop.java:18: \tArithmeticOperationRange assertion _JML__tmp`79 || (!(0 < _JML__tmp`77 && 0 < 1) || _JML__tmp`77 <= 2147483647 - 1)\n\t\t\tVALUE !(0 < _JML__tmp`77 && 0 < 1) || _JML__tmp`77 <= 2147483647 - 1\t === true\n/work/ForLoop.java:18: \tArithmeticOperationRange assertion _JML__tmp`81 || (!(_JML__tmp`77 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`77)\n\t\t\tVALUE !(_JML__tmp`77 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`77\t === true\n/work/ForLoop.java:19: \tx += 2\n\t\t\tVALUE 2\t === 2\n\t\t\tVALUE x += 2\t === ( - 5 )\n/work/ForLoop.java:19: \tArithmeticOperationRange assertion _JML__tmp`88 || (!(0 < _JML__tmp`86 && 0 < 2) || _JML__tmp`86 <= 2147483647 - 2)\n\t\t\tVALUE !(0 < _JML__tmp`86 && 0 < 2) || _JML__tmp`86 <= 2147483647 - 2\t === true\n/work/ForLoop.java:19: \tArithmeticOperationRange assertion _JML__tmp`90 || (!(_JML__tmp`86 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`86)\n\t\t\tVALUE !(_JML__tmp`86 < 0 && 2 < 0) || -2147483648 - 2 <= _JML__tmp`86\t === true\n/work/ForLoop.java:20: \ti++\n\t\t\tVALUE i\t === 5\n\t\t\tVALUE i++\t === 5\n/work/ForLoop.java:20: \tArithmeticOperationRange assertion _JML__tmp`98 || (!(0 < _JML__tmp`96 && 0 < 1) || _JML__tmp`96 <= 2147483647 - 1)\n\t\t\tVALUE !(0 < _JML__tmp`96 && 0 < 1) || _JML__tmp`96 <= 2147483647 - 1\t === true\n/work/ForLoop.java:20: \tArithmeticOperationRange assertion _JML__tmp`100 || (!(_JML__tmp`96 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`96)\n\t\t\tVALUE !(_JML__tmp`96 < 0 && 1 < 0) || -2147483648 - 1 <= _JML__tmp`96\t === true\n/work/ForLoop.java:22: \treturn x;\n/work/ForLoop.java:6: \tensures \\result == 0; \n\t\t\tVALUE \\result\t === ( - 5 )\n\t\t\tVALUE 0\t === 0\n\t\t\tVALUE \\result == 0\t === false\n/work/ForLoop.java:22: Invalid assertion (Postcondition)\n /work/ForLoop.java:6: Associated location\n%%ENDTRACE%%"
} ]
}
}
},
"performance" : {
"performance" : {
"ch.fhnw.autofeedback.MergeSortRunner" : {
"complexities" : [ "O(n)" ],
"measurements" : [ {
"problemSize" : 100000,
"runs" : 117,
"duration" : 2002
}, {
"problemSize" : 200000,
"runs" : 57,
"duration" : 2004
}, {
"problemSize" : 400000,
"runs" : 28,
"duration" : 2038
}, {
"problemSize" : 800000,
"runs" : 13,
"duration" : 2068
}, {
"problemSize" : 1040000,
"runs" : 10,
"duration" : 2175
}, {
"problemSize" : 1280000,
"runs" : 8,
"duration" : 2071
}, {
"problemSize" : 1520000,
"runs" : 7,
"duration" : 2105
}, {
"problemSize" : 1600000,
"runs" : 6,
"duration" : 2041
}, {
"problemSize" : 1760000,
"runs" : 6,
"duration" : 2117
}, {
"problemSize" : 2000000,
"runs" : 5,
"duration" : 2004
}, {
"problemSize" : 2240000,
"runs" : 5,
"duration" : 2288
}, {
"problemSize" : 2480000,
"runs" : 4,
"duration" : 2046
} ]
}
}
},
"unitTest" : {
"tests" : [ {
"name" : "testMax()",
"status" : "PASSED",
"message" : null
} ]
}
}
}