s05 skeletons, with some demo main()

tp-formals/src/s05/BoundedIntStack.java

 package s05;
 
+import java.util.Random;
+
 /* The capacity can't be negative. It's 
    forbidden to remove when empty, or to add
    when full. The collection cannot be empty
@@ -32,4 +34,41 @@ public class BoundedIntStack {
   public boolean isFull() {
     return top >= buf.length-1;
   }
+  
+  //------------------------------------------------------------------------
+  
+  public static boolean areAssertionsEnabled() {
+    int ec=0; 
+    assert (ec=1) == 1;
+    return ec == 1; 
+  }
+  
+  static Random rnd = new Random();
+  
+  static void playWithBoundedStack(BoundedIntStack s) {
+    int nOperations = 1000;
+    for(int i=0; i<nOperations; i++) {
+      boolean doPush = rnd.nextBoolean();
+      boolean doPop = !doPush;
+      if(doPush && !s.isFull())
+        s.push(rnd.nextInt());
+      if(doPop && !s.isEmpty())
+        s.pop();
+    }
+  }
+  
+  public static void main(String[] args) {
+    if(!areAssertionsEnabled()) {
+      System.out.println("Please enable assertions, with '-ea' VM option !!");
+      System.exit(-1);
+    }
+    int nStacks = 1000;
+    int maxSize = 50;
+    for(int i=0; i<nStacks; i++) {
+      BoundedIntStack s = new BoundedIntStack(rnd.nextInt(maxSize));
+      playWithBoundedStack(s);
+    }
+    System.out.println("End of demo!");
+  }
+
 }
\ No newline at end of file

tp-formals/src/s05/Ex4.java

+package s05;
+
+import java.util.Random;
+
+public class Ex4 {
+  // =================================
+  // For any:  int i;  F f,g; 
+  //   i == new F(i).a()
+  //   f.s(g).a() == f.a()+g.a()
+  static class F {
+    // TODO
+    public F(int i) {
+      // TODO 
+    }
+    public int a()  {
+      return 0; // TODO 
+    }
+    /*@ ensures \old(a()) == a() @*/
+    public F s(F y) {
+      return null; // TODO; 
+    }
+  }
+  // =================================
+  
+  //------------------------------------------------------------------
+  
+  public static boolean areAssertionsEnabled() {
+    int ec=0; 
+    assert (ec=1) == 1;
+    return ec == 1; 
+  }
+  
+  static Random rnd=new Random();
+  
+  // PRE: 0 < absMax < MAX_VALUE/2
+  static int rndIntIn(int absMax) {
+    return rnd.nextInt(2*absMax)-absMax;
+  }
+  
+  static void playWithClassF() {
+    int nOperations = 1000;
+    int max = 1000;
+    F f=new F(rndIntIn(max));
+    F g=new F(rndIntIn(max));
+    
+    for(int i=0; i<nOperations; i++) {
+      assert f.s(g).a() == f.a()+g.a();
+      int v = rndIntIn(max);
+      F h = new F(v);
+      assert v == h.a();
+      int fa = f.a();
+      int ga = g.a();
+      switch(rnd.nextInt(3)) {
+        case 0: h = f.s(g);
+        case 1: h = g.s(f);
+        case 2: break;
+      }
+      assert fa == f.a();
+      assert ga == g.a();
+      if(rnd.nextBoolean()) f = h;
+      else g = h;
+    }
+  }
+  
+  public static void main(String[] args) {
+    if(!areAssertionsEnabled()) {
+      System.out.println("Please enable assertions, with '-ea' VM option !!");
+      System.exit(-1);
+    }
+    playWithClassF();
+    System.out.println("End of demo!");
+  }
+
+}

tp-formals/src/s05/Ex5.java

+package s05;
+
+public class Ex5 {
+  // Compute ...  TODO  (b), informal description
+  static int cicr(int a) {
+    assert a >= 0;
+    int t=0, c=0, r=0; 
+    while(c <= a) {
+      assert c == r*r*r;
+      assert t == 3*r;
+      t = t + 3;
+      assert true;  // TODO
+      c = c + r*t + 1;
+      assert true;  // TODO
+      r = r + 1;
+    }
+    assert true;  // TODO (b), describe (r-1) formally
+    return r-1;
+  }
+  
+  //------------------------------------------------------------------------
+  
+  public static boolean areAssertionsEnabled() {
+    int ec=0; 
+    assert (ec=1) == 1;
+    return ec == 1; 
+  }
+  
+  public static void main(String[] args) {
+    if(!areAssertionsEnabled()) {
+      System.out.println("Please enable assertions, with '-ea' VM option !!");
+      System.exit(-1);
+    }
+    // Call cicr() with various parameters, just to see if assertions agree... 
+    int max = 570;
+    for(int i=0; i<max; i++) 
+      cicr(i);
+    System.out.println("End of demo!");
+  }
+  
+}