Final Push

ErzeugerVerbraucher/src/Buffer.java

 import java.util.concurrent.atomic.AtomicInteger;
 import java.util.concurrent.atomic.AtomicReferenceArray;
 
+
 /**
  * A generic and atomically safe Buffer data structure for holding values important in multithreaded use cases.
  * @param <T> The type of item to hold within the Buffer
@@ -18,6 +19,8 @@ public class Buffer<T> {
         this.items = new AtomicReferenceArray<>(size);
         this.itemCount = new AtomicInteger(0);
         this.size = size;
+
+        assert this.size >= 0 : "Size must be greater than 0";
     }
 
     /**

ErzeugerVerbraucher/src/Car.java

 public class Car {
+    /**
+     * Class Car
+     */
 }

ErzeugerVerbraucher/src/Consumer.java

@@ -14,6 +14,9 @@ public class Consumer implements Runnable {
      * @param asleep Boolean for Status
      * @param wakeCall Boolean for Status
      */
+    /**
+     "@Requires"({"buffer!=null","interval > 0","asleep!=null","wakeCall!=null", })
+     */
     public Consumer(Buffer<Car> buffer, int interval, AtomicBoolean asleep, AtomicBoolean wakeCall) {
         this.buffer = buffer;
         this.interval = interval;
@@ -23,7 +26,7 @@ public class Consumer implements Runnable {
 
     /**
      * Run function for the Consumer
-     * This Function checks randomly if the buffer has Cars and Pops them if that is the case.
+     * This Function checks randomly if the buffer has Workitems and Pops them if that is the case.
      * If the buffer is full it wakens the sleeping consumers.
      *
      */

ErzeugerVerbraucher/src/Producer.java

@@ -23,7 +23,7 @@ public class Producer implements Runnable {
 
     /**
      * Run Function for the Producer
-     * This function Produces Cars randomly when the Buffer is not full.
+     * This function Produces Workitems randomly when the Buffer is not full.
      * If the Buffer is empty it wakens the Sleeping Producers
      */
     @Override