/* 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 PriorityQueue_Contract {
	 declare parents : PriorityQueue implements Cloneable;
	public Object PriorityQueue.clone(){
		 try { 
			return super.clone();
				 } catch (Exception e){
					 System.out.println(" Error in cloning method");
					 e.printStackTrace();
					 return new Object(); 
				}
			}
		
		PriorityQueue old;
					 pointcut scope(): !within(PriorityQueue_Contract) && !cflow(withincode(* PriorityQueue_Contract.*(..)));
					 pointcut PriorityQueue_printQueue1(PriorityQueue trg_instance):call( public * PriorityQueue.printQueue(..))
							 && !call(public * (PriorityQueue+ && !PriorityQueue).printQueue(..)) && target(trg_instance) && scope();

			 pointcut cast_PriorityQueue_printQueue1(PriorityQueue trg_instance):!(call( public * PriorityQueue.printQueue(..)))
							 && execution(public * PriorityQueue.printQueue(..)) && !execution( public * (PriorityQueue+ && !PriorityQueue).printQueue(..)) && target(trg_instance) && scope();
			 pointcut PriorityQueue_printTree1(PriorityQueue trg_instance, PQ_Node node):call( public * PriorityQueue.printTree(..))
							 && !call(public * (PriorityQueue+ && !PriorityQueue).printTree(..)) && args(node) && target(trg_instance) && scope();

			 pointcut cast_PriorityQueue_printTree1(PriorityQueue trg_instance, PQ_Node node):!(call( public * PriorityQueue.printTree(..)))
							 && execution(public * PriorityQueue.printTree(..)) && !execution( public * (PriorityQueue+ && !PriorityQueue).printTree(..)) && args(node) && target(trg_instance) && scope();
			 pointcut PriorityQueue_enqueue1(PriorityQueue trg_instance, Object item):call( public * PriorityQueue.enqueue(..))
							 && !call(public * (PriorityQueue+ && !PriorityQueue).enqueue(..)) && args(item) && target(trg_instance) && scope();

			 pointcut cast_PriorityQueue_enqueue1(PriorityQueue trg_instance, Object item):!(call( public * PriorityQueue.enqueue(..)))
							 && execution(public * PriorityQueue.enqueue(..)) && !execution( public * (PriorityQueue+ && !PriorityQueue).enqueue(..)) && args(item) && target(trg_instance) && scope();
			 pointcut PriorityQueue_enqueue2(PriorityQueue trg_instance, Object item,int priority):call( public * PriorityQueue.enqueue(..))
							 && !call(public * (PriorityQueue+ && !PriorityQueue).enqueue(..)) && args(item,priority) && target(trg_instance) && scope();

			 pointcut cast_PriorityQueue_enqueue2(PriorityQueue trg_instance, Object item,int priority):!(call( public * PriorityQueue.enqueue(..)))
							 && execution(public * PriorityQueue.enqueue(..)) && !execution( public * (PriorityQueue+ && !PriorityQueue).enqueue(..)) && args(item,priority) && target(trg_instance) && scope();
			 pointcut PriorityQueue_splayLeft1(PriorityQueue trg_instance, PQ_Node node,PQ_Node lChild):call( public * PriorityQueue.splayLeft(..))
							 && !call(public * (PriorityQueue+ && !PriorityQueue).splayLeft(..)) && args(node,lChild) && target(trg_instance) && scope();

			 pointcut cast_PriorityQueue_splayLeft1(PriorityQueue trg_instance, PQ_Node node,PQ_Node lChild):!(call( public * PriorityQueue.splayLeft(..)))
							 && execution(public * PriorityQueue.splayLeft(..)) && !execution( public * (PriorityQueue+ && !PriorityQueue).splayLeft(..)) && args(node,lChild) && target(trg_instance) && scope();
			 pointcut PriorityQueue_splayRight1(PriorityQueue trg_instance, PQ_Node node,PQ_Node rChild):call( public * PriorityQueue.splayRight(..))
							 && !call(public * (PriorityQueue+ && !PriorityQueue).splayRight(..)) && args(node,rChild) && target(trg_instance) && scope();

			 pointcut cast_PriorityQueue_splayRight1(PriorityQueue trg_instance, PQ_Node node,PQ_Node rChild):!(call( public * PriorityQueue.splayRight(..)))
							 && execution(public * PriorityQueue.splayRight(..)) && !execution( public * (PriorityQueue+ && !PriorityQueue).splayRight(..)) && args(node,rChild) && target(trg_instance) && scope();
			 pointcut PriorityQueue_splayForInsert1(PriorityQueue trg_instance, PQ_Node newNode):call( public * PriorityQueue.splayForInsert(..))
							 && !call(public * (PriorityQueue+ && !PriorityQueue).splayForInsert(..)) && args(newNode) && target(trg_instance) && scope();

			 pointcut cast_PriorityQueue_splayForInsert1(PriorityQueue trg_instance, PQ_Node newNode):!(call( public * PriorityQueue.splayForInsert(..)))
							 && execution(public * PriorityQueue.splayForInsert(..)) && !execution( public * (PriorityQueue+ && !PriorityQueue).splayForInsert(..)) && args(newNode) && target(trg_instance) && scope();
			 pointcut PriorityQueue_dequeue1(PriorityQueue trg_instance):call( public * PriorityQueue.dequeue(..))
							 && !call(public * (PriorityQueue+ && !PriorityQueue).dequeue(..)) && target(trg_instance) && scope();

			 pointcut cast_PriorityQueue_dequeue1(PriorityQueue trg_instance):!(call( public * PriorityQueue.dequeue(..)))
							 && execution(public * PriorityQueue.dequeue(..)) && !execution( public * (PriorityQueue+ && !PriorityQueue).dequeue(..)) && target(trg_instance) && scope();
			 pointcut PriorityQueue_getMin1(PriorityQueue trg_instance):call( public * PriorityQueue.getMin(..))
							 && !call(public * (PriorityQueue+ && !PriorityQueue).getMin(..)) && target(trg_instance) && scope();

			 pointcut cast_PriorityQueue_getMin1(PriorityQueue trg_instance):!(call( public * PriorityQueue.getMin(..)))
							 && execution(public * PriorityQueue.getMin(..)) && !execution( public * (PriorityQueue+ && !PriorityQueue).getMin(..)) && target(trg_instance) && scope();

		
		
		
		
		
		before(PriorityQueue trg_instance , Object item ):
			PriorityQueue_enqueue1( trg_instance , item ){
				 boolean res = checkPre_enqueue( trg_instance , item);
				 boolean next =  checkPreHier_enqueue(trg_instance,item);
				 if (!res){
					System.out.println(" *** PRE CONDITION ERROR in  PriorityQueue in Method: enqueue");
					System.exit(1);
				}if (!next) { 
					System.out.println(" ***  PRE HIER ERROR in PriorityQueue in Method: enqueue");
					System.exit(1);
				}
			}
		before(PriorityQueue trg_instance , Object item ):
			cast_PriorityQueue_enqueue1( trg_instance, item ){
				String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
				String dynamicType = thisJoinPoint.getTarget().getClass().getName();
				
				 boolean hierResult = (Queue_Contract.aspectOf().checkPreHier_enqueue(trg_instance,item));
				
				 boolean res = checkPre_enqueue( trg_instance , item);
				
				if (hierResult && ! res){
					System.out.println(" **** CAST PRE HIER ERROR PriorityQueue in Method: enqueue");
					 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
				}
			}
			
			before(PriorityQueue trg_instance , Object item,int priority ):
				PriorityQueue_enqueue2( trg_instance , item,priority ){
					 boolean res = checkPre_enqueue( trg_instance , item,priority);
					 boolean next =  true ;
					 if (!res){
						System.out.println(" *** PRE CONDITION ERROR in  PriorityQueue in Method: enqueue");
						System.exit(1);
					}if (!next) { 
						System.out.println(" ***  PRE HIER ERROR in PriorityQueue in Method: enqueue");
						System.exit(1);
					}
				}
			before(PriorityQueue trg_instance , Object item,int priority ):
				cast_PriorityQueue_enqueue2( trg_instance, item,priority ){
					String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
					String dynamicType = thisJoinPoint.getTarget().getClass().getName();
					
					 boolean hierResult = (true);
					
					 boolean res = checkPre_enqueue( trg_instance , item,priority);
					
					if (hierResult && ! res){
						System.out.println(" **** CAST PRE HIER ERROR PriorityQueue in Method: enqueue");
						 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
					}
				}
				
				before(PriorityQueue trg_instance , PQ_Node node,PQ_Node lChild ):
					PriorityQueue_splayLeft1( trg_instance , node,lChild ){
						 boolean res = checkPre_splayLeft( trg_instance , node,lChild);
						 boolean next =  true ;
						 if (!res){
							System.out.println(" *** PRE CONDITION ERROR in  PriorityQueue in Method: splayLeft");
							System.exit(1);
						}if (!next) { 
							System.out.println(" ***  PRE HIER ERROR in PriorityQueue in Method: splayLeft");
							System.exit(1);
						}
					}
				before(PriorityQueue trg_instance , PQ_Node node,PQ_Node lChild ):
					cast_PriorityQueue_splayLeft1( trg_instance, node,lChild ){
						String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
						String dynamicType = thisJoinPoint.getTarget().getClass().getName();
						
						 boolean hierResult = (true);
						
						 boolean res = checkPre_splayLeft( trg_instance , node,lChild);
						
						if (hierResult && ! res){
							System.out.println(" **** CAST PRE HIER ERROR PriorityQueue in Method: splayLeft");
							 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
						}
					}
					
					before(PriorityQueue trg_instance , PQ_Node node,PQ_Node rChild ):
						PriorityQueue_splayRight1( trg_instance , node,rChild ){
							 boolean res = checkPre_splayRight( trg_instance , node,rChild);
							 boolean next =  true ;
							 if (!res){
								System.out.println(" *** PRE CONDITION ERROR in  PriorityQueue in Method: splayRight");
								System.exit(1);
							}if (!next) { 
								System.out.println(" ***  PRE HIER ERROR in PriorityQueue in Method: splayRight");
								System.exit(1);
							}
						}
					before(PriorityQueue trg_instance , PQ_Node node,PQ_Node rChild ):
						cast_PriorityQueue_splayRight1( trg_instance, node,rChild ){
							String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
							String dynamicType = thisJoinPoint.getTarget().getClass().getName();
							
							 boolean hierResult = (true);
							
							 boolean res = checkPre_splayRight( trg_instance , node,rChild);
							
							if (hierResult && ! res){
								System.out.println(" **** CAST PRE HIER ERROR PriorityQueue in Method: splayRight");
								 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
							}
						}
						
						before(PriorityQueue trg_instance , PQ_Node newNode ):
							PriorityQueue_splayForInsert1( trg_instance , newNode ){
								 boolean res = checkPre_splayForInsert( trg_instance , newNode);
								 boolean next =  true ;
								 if (!res){
									System.out.println(" *** PRE CONDITION ERROR in  PriorityQueue in Method: splayForInsert");
									System.exit(1);
								}if (!next) { 
									System.out.println(" ***  PRE HIER ERROR in PriorityQueue in Method: splayForInsert");
									System.exit(1);
								}
							}
						before(PriorityQueue trg_instance , PQ_Node newNode ):
							cast_PriorityQueue_splayForInsert1( trg_instance, newNode ){
								String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
								String dynamicType = thisJoinPoint.getTarget().getClass().getName();
								
								 boolean hierResult = (true);
								
								 boolean res = checkPre_splayForInsert( trg_instance , newNode);
								
								if (hierResult && ! res){
									System.out.println(" **** CAST PRE HIER ERROR PriorityQueue in Method: splayForInsert");
									 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
								}
							}
							
							before(PriorityQueue trg_instance  ):
								PriorityQueue_dequeue1( trg_instance  ){
									 boolean res = checkPre_dequeue( trg_instance );
									 boolean next =  checkPreHier_dequeue(trg_instance);
									 if (!res){
										System.out.println(" *** PRE CONDITION ERROR in  PriorityQueue in Method: dequeue");
										System.exit(1);
									}if (!next) { 
										System.out.println(" ***  PRE HIER ERROR in PriorityQueue in Method: dequeue");
										System.exit(1);
									}
								}
							before(PriorityQueue trg_instance  ):
								cast_PriorityQueue_dequeue1( trg_instance ){
									String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
									String dynamicType = thisJoinPoint.getTarget().getClass().getName();
									
									 boolean hierResult = (Queue_Contract.aspectOf().checkPreHier_dequeue(trg_instance));
									
									 boolean res = checkPre_dequeue( trg_instance );
									
									if (hierResult && ! res){
										System.out.println(" **** CAST PRE HIER ERROR PriorityQueue in Method: dequeue");
										 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
									}
								}
								
								before(PriorityQueue trg_instance  ):
									PriorityQueue_getMin1( trg_instance  ){
										 boolean res = checkPre_getMin( trg_instance );
										 boolean next =  true ;
										 if (!res){
											System.out.println(" *** PRE CONDITION ERROR in  PriorityQueue in Method: getMin");
											System.exit(1);
										}if (!next) { 
											System.out.println(" ***  PRE HIER ERROR in PriorityQueue in Method: getMin");
											System.exit(1);
										}
									}
								before(PriorityQueue trg_instance  ):
									cast_PriorityQueue_getMin1( trg_instance ){
										String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
										String dynamicType = thisJoinPoint.getTarget().getClass().getName();
										
										 boolean hierResult = (true);
										
										 boolean res = checkPre_getMin( trg_instance );
										
										if (hierResult && ! res){
											System.out.println(" **** CAST PRE HIER ERROR PriorityQueue in Method: getMin");
											 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
										}
									}
									
									
									
									
									
									public boolean checkPre_enqueue(PriorityQueue trg_instance,Object item){
										if(trg_instance.size<trg_instance.capacity)
											return true;
										else
											return false;
										}
									public boolean checkPreHier_enqueue(PriorityQueue trg_instance,Object item){
										
											 boolean myPre = checkPre_enqueue( trg_instance , item);
											 boolean hierarchy  = (Queue_Contract.aspectOf().checkPreHier_enqueue(trg_instance,item));
											
											if (!hierarchy || myPre)
												 return myPre; 
											else
												 return false;
											}
											
											public boolean checkPre_enqueue(PriorityQueue trg_instance,Object item,int priority){
												if(trg_instance.size<trg_instance.capacity)
													return true;
												else
													return false;
												}
											public boolean checkPreHier_enqueue(PriorityQueue trg_instance,Object item,int priority){
												
													 boolean myPre = checkPre_enqueue( trg_instance , item,priority);
													 boolean hierarchy  = (true);
													
													if (!hierarchy || myPre)
														 return myPre; 
													else
														 return false;
													}
													
													public boolean checkPre_splayLeft(PriorityQueue trg_instance,PQ_Node node,PQ_Node lChild){
														if(lChild!=null)
															return true;
														else
															return false;
														}
													public boolean checkPreHier_splayLeft(PriorityQueue trg_instance,PQ_Node node,PQ_Node lChild){
														
															 boolean myPre = checkPre_splayLeft( trg_instance , node,lChild);
															 boolean hierarchy  = (true);
															
															if (!hierarchy || myPre)
																 return myPre; 
															else
																 return false;
															}
															
															public boolean checkPre_splayRight(PriorityQueue trg_instance,PQ_Node node,PQ_Node rChild){
																if(rChild!=null)
																	return true;
																else
																	return false;
																}
															public boolean checkPreHier_splayRight(PriorityQueue trg_instance,PQ_Node node,PQ_Node rChild){
																
																	 boolean myPre = checkPre_splayRight( trg_instance , node,rChild);
																	 boolean hierarchy  = (true);
																	
																	if (!hierarchy || myPre)
																		 return myPre; 
																	else
																		 return false;
																	}
																	
																	public boolean checkPre_splayForInsert(PriorityQueue trg_instance,PQ_Node newNode){
																		if(newNode!=null)
																			return true;
																		else
																			return false;
																		}
																	public boolean checkPreHier_splayForInsert(PriorityQueue trg_instance,PQ_Node newNode){
																		
																			 boolean myPre = checkPre_splayForInsert( trg_instance , newNode);
																			 boolean hierarchy  = (true);
																			
																			if (!hierarchy || myPre)
																				 return myPre; 
																			else
																				 return false;
																			}
																			
																			public boolean checkPre_dequeue(PriorityQueue trg_instance){
																				if(trg_instance.root!=null)
																					return true;
																				else
																					return false;
																				}
																			public boolean checkPreHier_dequeue(PriorityQueue trg_instance){
																				
																					 boolean myPre = checkPre_dequeue( trg_instance );
																					 boolean hierarchy  = (Queue_Contract.aspectOf().checkPreHier_dequeue(trg_instance));
																					
																					if (!hierarchy || myPre)
																						 return myPre; 
																					else
																						 return false;
																					}
																					
																					public boolean checkPre_getMin(PriorityQueue trg_instance){
																						if(trg_instance.root!=null)
																							return true;
																						else
																							return false;
																						}
																					public boolean checkPreHier_getMin(PriorityQueue trg_instance){
																						
																							 boolean myPre = checkPre_getMin( trg_instance );
																							 boolean hierarchy  = (true);
																							
																							if (!hierarchy || myPre)
																								 return myPre; 
																							else
																								 return false;
																							}
																							}