LHospital13 commited on
Commit
68c2dba
1 Parent(s): 60678d4

Update samples/AddLoop-v3.java

Browse files
Files changed (1) hide show
  1. samples/AddLoop-v3.java +4 -2
samples/AddLoop-v3.java CHANGED
@@ -4,7 +4,8 @@ public class AddLoop {
4
  int sum = x;
5
  if (y > 0) {
6
  int n = y;
7
- //@ maintaining sum == x + (y - n) && n >= 0;
 
8
  //@ decreases n;
9
  while (n > 0) {
10
  sum = sum + 1;
@@ -12,7 +13,8 @@ public class AddLoop {
12
  }
13
  } else {
14
  int n = -y;
15
- //@ maintaining sum == x + (y + n) && n >= 0;
 
16
  //@ decreases n;
17
  while (n > 0) {
18
  sum = sum - 1;
 
4
  int sum = x;
5
  if (y > 0) {
6
  int n = y;
7
+ //@ maintaining sum == x + (y - n);
8
+ //@ maintaining n >= 0;
9
  //@ decreases n;
10
  while (n > 0) {
11
  sum = sum + 1;
 
13
  }
14
  } else {
15
  int n = -y;
16
+ //@ maintaining sum == x + (y + n);
17
+ //@ maintaining n >= 0;
18
  //@ decreases n;
19
  while (n > 0) {
20
  sum = sum - 1;