content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.util.concurrent;
  
  public interface ExecutorService extends java.util.concurrent.Executor
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public void shutdown();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.util.List shutdownNow();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isShutdown();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isTerminated();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InterruptedException e) true; */
     public boolean awaitTermination(long arg0, java.util.concurrent.TimeUnit arg1) throws java.lang.InterruptedException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.util.concurrent.Future submit(java.util.concurrent.Callable arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.util.concurrent.Future submit(java.lang.Runnable arg0, java.lang.Object arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.util.concurrent.Future submit(java.lang.Runnable arg0);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InterruptedException e) true; */
     public java.util.List invokeAll(java.util.Collection arg0) throws java.lang.InterruptedException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InterruptedException e) true; */
     public java.util.List invokeAll(java.util.Collection arg0, long arg1, java.util.concurrent.TimeUnit arg2) throws java.lang.InterruptedException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InterruptedException e) true; signals (java.util.concurrent.ExecutionException e) true; */
     public java.lang.Object invokeAny(java.util.Collection arg0) throws java.lang.InterruptedException, java.util.concurrent.ExecutionException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InterruptedException e) true; signals (java.util.concurrent.ExecutionException e) true; signals (java.util.concurrent.TimeoutException e) true; */
     public java.lang.Object invokeAny(java.util.Collection arg0, long arg1, java.util.concurrent.TimeUnit arg2) throws java.lang.InterruptedException, java.util.concurrent.ExecutionException, java.util.concurrent.TimeoutException;
  }
  