Commit 213ed260 authored by Lulu Luong's avatar Lulu Luong

added small Java example : SumPositive

parent efa414a4
Pipeline #30481 failed with stages
in 2 seconds
package edu.kit.iti.formal.psdbg.examples.java.sumPositive;
import edu.kit.iti.formal.psdbg.examples.JavaExample;
public class SumPositiveExample extends JavaExample {
public SumPositiveExample () {
setName("SumPositive example");
setJavaFile(getClass().
getResource("SumPositive.java"));
setScriptFile(getClass().
getResource("script.kps"));
}
}
......@@ -5,6 +5,7 @@ edu.kit.iti.formal.psdbg.examples.java.maxtriplet.MaxTripletExample
#edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample
#edu.kit.iti.formal.psdbg.examples.java.dpqs.DualPivotExample
edu.kit.iti.formal.psdbg.examples.java.quicksort.QuickSort
edu.kit.iti.formal.psdbg.examples.java.sumPositive.SumPositiveExample
edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample
#edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample
#edu.kit.iti.formal.psdbg.examples.java.sumAndMax.SumAndMaxExample
......
package edu.kit.iti.formal.psdbg.examples.java.sumPositive;
public class SumPositive{
/*@ public normal_behaviour
@ requires a != null;
@ ensures \result >= 0;
@*/
public int sumPositiveArray(int[] a) {
int sum = 0;
/*@
@ loop_invariant 0 <= i && i <= a.length;
@ loop_invariant \old(sum) <= sum;
@ decreases a.length - i;
@ assignable sum;
@*/
for (int i = 0; i < a.length; i++) {
if(a[i] >= 0) {
sum += a[i];
}
}
return sum;
}
}
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment