/* This file was generated by Contract AspectJ v0.1 on Sat Nov 06 14:12:10 EST 2004 */
 /** CONAJ: Original packages **/
package jsim.queue;
 /** CONAJ: Imports needed by CONAJ  **/
 import org.aspectj.lang.*; 
 import java.util.*;
 /** CONAJ: Original imports **/



	 privileged aspect Queue_Contract {
	 declare parents : Queue implements Cloneable;
	public Object Queue.clone(){
		 try { 
			return super.clone();
				 } catch (Exception e){
					 System.out.println(" Error in cloning method");
					 e.printStackTrace();
					 return new Object(); 
				}
			}
		
		Queue old;
					 pointcut scope(): !within(Queue_Contract) && !cflow(withincode(* Queue_Contract.*(..)));
					 pointcut Queue_empty1(Queue trg_instance):call( public * Queue.empty(..))
							 && !call(public * (Queue+ && !Queue).empty(..)) && target(trg_instance) && scope();

			 pointcut cast_Queue_empty1(Queue trg_instance):!(call( public * Queue.empty(..)))
							 && execution(public * Queue.empty(..)) && !execution( public * (Queue+ && !Queue).empty(..)) && target(trg_instance) && scope();
			 pointcut Queue_full1(Queue trg_instance):call( public * Queue.full(..))
							 && !call(public * (Queue+ && !Queue).full(..)) && target(trg_instance) && scope();

			 pointcut cast_Queue_full1(Queue trg_instance):!(call( public * Queue.full(..)))
							 && execution(public * Queue.full(..)) && !execution( public * (Queue+ && !Queue).full(..)) && target(trg_instance) && scope();
			 pointcut Queue_length1(Queue trg_instance):call( public * Queue.length(..))
							 && !call(public * (Queue+ && !Queue).length(..)) && target(trg_instance) && scope();

			 pointcut cast_Queue_length1(Queue trg_instance):!(call( public * Queue.length(..)))
							 && execution(public * Queue.length(..)) && !execution( public * (Queue+ && !Queue).length(..)) && target(trg_instance) && scope();
			 pointcut Queue_front1(Queue trg_instance):call( public * Queue.front(..))
							 && !call(public * (Queue+ && !Queue).front(..)) && target(trg_instance) && scope();

			 pointcut cast_Queue_front1(Queue trg_instance):!(call( public * Queue.front(..)))
							 && execution(public * Queue.front(..)) && !execution( public * (Queue+ && !Queue).front(..)) && target(trg_instance) && scope();
			 pointcut Queue_cancel1(Queue trg_instance, Q_Node node):call( public * Queue.cancel(..))
							 && !call(public * (Queue+ && !Queue).cancel(..)) && args(node) && target(trg_instance) && scope();

			 pointcut cast_Queue_cancel1(Queue trg_instance, Q_Node node):!(call( public * Queue.cancel(..)))
							 && execution(public * Queue.cancel(..)) && !execution( public * (Queue+ && !Queue).cancel(..)) && args(node) && target(trg_instance) && scope();
			 pointcut Queue_dequeue1(Queue trg_instance):call( public * Queue.dequeue(..))
							 && !call(public * (Queue+ && !Queue).dequeue(..)) && target(trg_instance) && scope();

			 pointcut cast_Queue_dequeue1(Queue trg_instance):!(call( public * Queue.dequeue(..)))
							 && execution(public * Queue.dequeue(..)) && !execution( public * (Queue+ && !Queue).dequeue(..)) && target(trg_instance) && scope();
			 pointcut Queue_removeMin1(Queue trg_instance):call( public * Queue.removeMin(..))
							 && !call(public * (Queue+ && !Queue).removeMin(..)) && target(trg_instance) && scope();

			 pointcut cast_Queue_removeMin1(Queue trg_instance):!(call( public * Queue.removeMin(..)))
							 && execution(public * Queue.removeMin(..)) && !execution( public * (Queue+ && !Queue).removeMin(..)) && target(trg_instance) && scope();
			 pointcut Queue_clear1(Queue trg_instance):call( public * Queue.clear(..))
							 && !call(public * (Queue+ && !Queue).clear(..)) && target(trg_instance) && scope();

			 pointcut cast_Queue_clear1(Queue trg_instance):!(call( public * Queue.clear(..)))
							 && execution(public * Queue.clear(..)) && !execution( public * (Queue+ && !Queue).clear(..)) && target(trg_instance) && scope();
			 pointcut Queue_enqueue1(Queue trg_instance, Object item):call( public * Queue.enqueue(..))
							 && !call(public * (Queue+ && !Queue).enqueue(..)) && args(item) && target(trg_instance) && scope();

			 pointcut cast_Queue_enqueue1(Queue trg_instance, Object item):!(call( public * Queue.enqueue(..)))
							 && execution(public * Queue.enqueue(..)) && !execution( public * (Queue+ && !Queue).enqueue(..)) && args(item) && target(trg_instance) && scope();

		
		
		
		
		
		
		
		before(Queue trg_instance  ):
			Queue_front1( trg_instance  ){
				 boolean res = checkPre_front( trg_instance );
				 boolean next =  true ;
				 if (!res){
					System.out.println(" *** PRE CONDITION ERROR in  Queue in Method: front");
					System.exit(1);
				}if (!next) { 
					System.out.println(" ***  PRE HIER ERROR in Queue in Method: front");
					System.exit(1);
				}
			}
		before(Queue trg_instance  ):
			cast_Queue_front1( trg_instance ){
				String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
				String dynamicType = thisJoinPoint.getTarget().getClass().getName();
				
				 boolean hierResult = (true);
				
				 boolean res = checkPre_front( trg_instance );
				
				if (hierResult && ! res){
					System.out.println(" **** CAST PRE HIER ERROR Queue in Method: front");
					 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
				}
			}
			
			before(Queue trg_instance , Q_Node node ):
				Queue_cancel1( trg_instance , node ){
					 boolean res = checkPre_cancel( trg_instance , node);
					 boolean next =  true ;
					 if (!res){
						System.out.println(" *** PRE CONDITION ERROR in  Queue in Method: cancel");
						System.exit(1);
					}if (!next) { 
						System.out.println(" ***  PRE HIER ERROR in Queue in Method: cancel");
						System.exit(1);
					}
				}
			before(Queue trg_instance , Q_Node node ):
				cast_Queue_cancel1( trg_instance, node ){
					String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
					String dynamicType = thisJoinPoint.getTarget().getClass().getName();
					
					 boolean hierResult = (true);
					
					 boolean res = checkPre_cancel( trg_instance , node);
					
					if (hierResult && ! res){
						System.out.println(" **** CAST PRE HIER ERROR Queue in Method: cancel");
						 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
					}
				}
				
				before(Queue trg_instance  ):
					Queue_dequeue1( trg_instance  ){
						 boolean res = checkPre_dequeue( trg_instance );
						 boolean next =  true ;
						 if (!res){
							System.out.println(" *** PRE CONDITION ERROR in  Queue in Method: dequeue");
							System.exit(1);
						}if (!next) { 
							System.out.println(" ***  PRE HIER ERROR in Queue in Method: dequeue");
							System.exit(1);
						}
					}
				before(Queue trg_instance  ):
					cast_Queue_dequeue1( trg_instance ){
						String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
						String dynamicType = thisJoinPoint.getTarget().getClass().getName();
						
						 boolean hierResult = (true);
						
						 boolean res = checkPre_dequeue( trg_instance );
						
						if (hierResult && ! res){
							System.out.println(" **** CAST PRE HIER ERROR Queue in Method: dequeue");
							 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
						}
					}
					
					before(Queue trg_instance  ):
						Queue_removeMin1( trg_instance  ){
							 boolean res = checkPre_removeMin( trg_instance );
							 boolean next =  true ;
							 if (!res){
								System.out.println(" *** PRE CONDITION ERROR in  Queue in Method: removeMin");
								System.exit(1);
							}if (!next) { 
								System.out.println(" ***  PRE HIER ERROR in Queue in Method: removeMin");
								System.exit(1);
							}
						}
					before(Queue trg_instance  ):
						cast_Queue_removeMin1( trg_instance ){
							String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
							String dynamicType = thisJoinPoint.getTarget().getClass().getName();
							
							 boolean hierResult = (true);
							
							 boolean res = checkPre_removeMin( trg_instance );
							
							if (hierResult && ! res){
								System.out.println(" **** CAST PRE HIER ERROR Queue in Method: removeMin");
								 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
							}
						}
						
						
						
						before(Queue trg_instance , Object item ):
							Queue_enqueue1( trg_instance , item ){
								 boolean res = checkPre_enqueue( trg_instance , item);
								 boolean next =  true ;
								 if (!res){
									System.out.println(" *** PRE CONDITION ERROR in  Queue in Method: enqueue");
									System.exit(1);
								}if (!next) { 
									System.out.println(" ***  PRE HIER ERROR in Queue in Method: enqueue");
									System.exit(1);
								}
							}
						before(Queue trg_instance , Object item ):
							cast_Queue_enqueue1( trg_instance, item ){
								String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
								String dynamicType = thisJoinPoint.getTarget().getClass().getName();
								
								 boolean hierResult = (true);
								
								 boolean res = checkPre_enqueue( trg_instance , item);
								
								if (hierResult && ! res){
									System.out.println(" **** CAST PRE HIER ERROR Queue in Method: enqueue");
									 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
								}
							}
							
							
							
							
							
							
							
							public boolean checkPre_front(Queue trg_instance){
								if(trg_instance.root!=null)
									return true;
								else
									return false;
								}
							public boolean checkPreHier_front(Queue trg_instance){
								
									 boolean myPre = checkPre_front( trg_instance );
									 boolean hierarchy  = (true);
									
									if (!hierarchy || myPre)
										 return myPre; 
									else
										 return false;
									}
									
									public boolean checkPre_cancel(Queue trg_instance,Q_Node node){
										if(node!=null)
											return true;
										else
											return false;
										}
									public boolean checkPreHier_cancel(Queue trg_instance,Q_Node node){
										
											 boolean myPre = checkPre_cancel( trg_instance , node);
											 boolean hierarchy  = (true);
											
											if (!hierarchy || myPre)
												 return myPre; 
											else
												 return false;
											}
											
											public boolean checkPre_dequeue(Queue trg_instance){
												if(trg_instance.root!=null)
													return true;
												else
													return false;
												}
											public boolean checkPreHier_dequeue(Queue trg_instance){
												
													 boolean myPre = checkPre_dequeue( trg_instance );
													 boolean hierarchy  = (true);
													
													if (!hierarchy || myPre)
														 return myPre; 
													else
														 return false;
													}
													
													public boolean checkPre_removeMin(Queue trg_instance){
														if(trg_instance.root!=null)
															return true;
														else
															return false;
														}
													public boolean checkPreHier_removeMin(Queue trg_instance){
														
															 boolean myPre = checkPre_removeMin( trg_instance );
															 boolean hierarchy  = (true);
															
															if (!hierarchy || myPre)
																 return myPre; 
															else
																 return false;
															}
															
															
															
															public boolean checkPre_enqueue(Queue trg_instance,Object item){
																if(true)
																	return true;
																else
																	return false;
																}
															public boolean checkPreHier_enqueue(Queue trg_instance,Object item){
																
																	 boolean myPre = checkPre_enqueue( trg_instance , item);
																	 boolean hierarchy  = (true);
																	
																	if (!hierarchy || myPre)
																		 return myPre; 
																	else
																		 return false;
																	}
																	}