/* This file was generated by Contract AspectJ v0.1 on Mon Oct 18 16:06:47 EDT 2004 */
 /** CONAJ: Original packages **/
 /** CONAJ: Imports needed by CONAJ  **/
 import org.aspectj.lang.*; 
 import java.util.*;
 /** CONAJ: Original imports **/
import java.util.Vector;
import java.util.Iterator;
import java.io.StringWriter;



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

			 pointcut cast_MyStack_size(MyStack trg_instance):!(call( public * MyStack.size(..)))
							 && execution(public * MyStack.size(..)) && !execution( public * (MyStack+ && !MyStack).size(..)) && target(trg_instance) && scope();
			 pointcut MyStack_push(MyStack trg_instance, int i):call( public * MyStack.push(..))
							 && !call(public * (MyStack+ && !MyStack).push(..)) && args(i) && target(trg_instance) && scope();

			 pointcut cast_MyStack_push(MyStack trg_instance, int i):!(call( public * MyStack.push(..)))
							 && execution(public * MyStack.push(..)) && !execution( public * (MyStack+ && !MyStack).push(..)) && args(i) && target(trg_instance) && scope();
			 pointcut MyStack_pop(MyStack trg_instance):call( public * MyStack.pop(..))
							 && !call(public * (MyStack+ && !MyStack).pop(..)) && target(trg_instance) && scope();

			 pointcut cast_MyStack_pop(MyStack trg_instance):!(call( public * MyStack.pop(..)))
							 && execution(public * MyStack.pop(..)) && !execution( public * (MyStack+ && !MyStack).pop(..)) && target(trg_instance) && scope();
			 pointcut MyStack_top(MyStack trg_instance):call( public * MyStack.top(..))
							 && !call(public * (MyStack+ && !MyStack).top(..)) && target(trg_instance) && scope();

			 pointcut cast_MyStack_top(MyStack trg_instance):!(call( public * MyStack.top(..)))
							 && execution(public * MyStack.top(..)) && !execution( public * (MyStack+ && !MyStack).top(..)) && target(trg_instance) && scope();
			 pointcut MyStack_full(MyStack trg_instance):call( public * MyStack.full(..))
							 && !call(public * (MyStack+ && !MyStack).full(..)) && target(trg_instance) && scope();

			 pointcut cast_MyStack_full(MyStack trg_instance):!(call( public * MyStack.full(..)))
							 && execution(public * MyStack.full(..)) && !execution( public * (MyStack+ && !MyStack).full(..)) && target(trg_instance) && scope();
			 pointcut MyStack_empty(MyStack trg_instance):call( public * MyStack.empty(..))
							 && !call(public * (MyStack+ && !MyStack).empty(..)) && target(trg_instance) && scope();

			 pointcut cast_MyStack_empty(MyStack trg_instance):!(call( public * MyStack.empty(..)))
							 && execution(public * MyStack.empty(..)) && !execution( public * (MyStack+ && !MyStack).empty(..)) && target(trg_instance) && scope();
			 pointcut MyStack_printMe(MyStack trg_instance):call( public * MyStack.printMe(..))
							 && !call(public * (MyStack+ && !MyStack).printMe(..)) && target(trg_instance) && scope();

			 pointcut cast_MyStack_printMe(MyStack trg_instance):!(call( public * MyStack.printMe(..)))
							 && execution(public * MyStack.printMe(..)) && !execution( public * (MyStack+ && !MyStack).printMe(..)) && target(trg_instance) && scope();

 // PCD for Invariant
			 pointcut MyStack_invariant(MyStack trg_instance):call(public * MyStack.*(..)) && !call(public * (MyStack+ && !MyStack).*(..)) && target(trg_instance) && scope();

		before(MyStack trg_instance):
			MyStack_invariant(trg_instance){
				if (!checkInvariant(trg_instance)){
					System.out.println("error in inv before a method call");
					System.exit(1);
				}
			}
		
		
		
		
		before(MyStack trg_instance , int i ):
			MyStack_push( trg_instance , i ){
				old = (MyStack) trg_instance.clone();
				 boolean res = checkPre_push( trg_instance , i);
				 boolean next =  true ;
				 if (!res){
					System.out.println(" *** PRE CONDITION ERROR in  MyStack in Method: push");
					System.exit(1);
				}if (!next) { 
					System.out.println(" ***  PRE HIER ERROR in MyStack in Method: push");
					System.exit(1);
				}
			}
		before(MyStack trg_instance , int i ):
			cast_MyStack_push( trg_instance, i ){
				String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
				String dynamicType = thisJoinPoint.getTarget().getClass().getName();
				
				 boolean hierResult = (true);
				
				 boolean res = checkPre_push( trg_instance , i);
				
				if (hierResult && ! res){
					System.out.println(" **** CAST PRE HIER ERROR MyStack in Method: push");
					 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
				}
			}after(MyStack trg_instance , int i ):
				MyStack_push( trg_instance, i ) {
					 boolean res = checkPost_push( trg_instance, i);
					if(!res){
						System.out.println("Failed in post condition in: MyStack in Method: push");
						System.out.println("Exiting ... ");
						System.exit(1);
					}
					boolean postHier = checkPostHier_push(trg_instance, res,i);
					if(!postHier){
						System.out.println("Failed in post hier in: MyStack in Method: push ");
						System.exit(1);
					}
				}
				after(MyStack trg_instance , int i ):
					cast_MyStack_push( trg_instance, i ){
						 boolean postResult = checkPost_push( trg_instance, i);
						if(!postResult){
							System.out.println("Failed in post condition in: MyStack in Method: push");
							System.out.println("Exiting ... ");
							System.exit(1);
						}
						boolean postHier = (true);
					
					if(!postHier){
						System.out.println("Failed in post hier in: MyStack in Method: push ");
						String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
						String dynamicType = thisJoinPoint.getTarget().getClass().getName();
						
						System.out.println(" **** CAST POST HIER ERROR MyStack in Method: push");
						 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
					}
				}
				
				before(MyStack trg_instance  ):
					MyStack_pop( trg_instance  ){
						old = (MyStack) trg_instance.clone();
						 boolean res = checkPre_pop( trg_instance );
						 boolean next =  true ;
						 if (!res){
							System.out.println(" *** PRE CONDITION ERROR in  MyStack in Method: pop");
							System.exit(1);
						}if (!next) { 
							System.out.println(" ***  PRE HIER ERROR in MyStack in Method: pop");
							System.exit(1);
						}
					}
				before(MyStack trg_instance  ):
					cast_MyStack_pop( trg_instance ){
						String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
						String dynamicType = thisJoinPoint.getTarget().getClass().getName();
						
						 boolean hierResult = (true);
						
						 boolean res = checkPre_pop( trg_instance );
						
						if (hierResult && ! res){
							System.out.println(" **** CAST PRE HIER ERROR MyStack in Method: pop");
							 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
						}
					}after(MyStack trg_instance  ) returning (int result):
						MyStack_pop( trg_instance ) {
							 boolean res = checkPost_pop( trg_instance, result);
							if(!res){
								System.out.println("Failed in post condition in: MyStack in Method: pop");
								System.out.println("Exiting ... ");
								System.exit(1);
							}
							boolean postHier = checkPostHier_pop(trg_instance, res, result);
							if(!postHier){
								System.out.println("Failed in post hier in: MyStack in Method: pop ");
								System.exit(1);
							}
						}
						after(MyStack trg_instance  ) returning (int result):
							cast_MyStack_pop( trg_instance ){
								 boolean postResult = checkPost_pop( trg_instance, result);
								if(!postResult){
									System.out.println("Failed in post condition in: MyStack in Method: pop");
									System.out.println("Exiting ... ");
									System.exit(1);
								}
								boolean postHier = (true);
							
							if(!postHier){
								System.out.println("Failed in post hier in: MyStack in Method: pop ");
								String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
								String dynamicType = thisJoinPoint.getTarget().getClass().getName();
								
								System.out.println(" **** CAST POST HIER ERROR MyStack in Method: pop");
								 System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" **** dynamicType "+dynamicType+" SIG ==> "+ thisJoinPoint.getSignature().toLongString());System.exit(1);
							}
						}
						
						
						
						
						
						
						
						
						after(MyStack trg_instance):
							MyStack_invariant(trg_instance){
								if (!checkInvariant(trg_instance)){
									System.out.println("error in inv after a method call");
									System.exit(1);
								}
							}
						
 public boolean checkInvariant(MyStack trg_instance){
							if (0<=trg_instance.size()&&trg_instance.size()<=trg_instance.maxSize) {
			 return true;
			} else { 
			 return false;
			}

						}
					
					
					
					
					public boolean checkPre_push(MyStack trg_instance,int i){
						if(!trg_instance.full())
							return true;
						else
							return false;
						}
					public boolean checkPost_push(MyStack trg_instance,int i){
						if(  ! trg_instance.empty() &&  trg_instance.top() == i &&  trg_instance.size() == old.size() + 1  )
							return true;
						else
							return false;
						}
					public boolean checkPreHier_push(MyStack trg_instance,int i){
						
							 boolean myPre = checkPre_push( trg_instance , i);
							 boolean hierarchy  = (true);
							
							if (!hierarchy || myPre)
								 return myPre; 
							else
								 return false;
							}public boolean checkPostHier_push(MyStack trg_instance, boolean last,int i){
								
							boolean postResult = checkPost_push( trg_instance, i);
							if (!last || postResult){
								 return (true);
							
						}else 
							return false;
						}
						
						public boolean checkPre_pop(MyStack trg_instance){
							if(!trg_instance.empty())
								return true;
							else
								return false;
							}
						public boolean checkPost_pop(MyStack trg_instance, int result){
							if(  ! trg_instance.full() &&  trg_instance.size() == old.size() - 1  )
								return true;
							else
								return false;
							}
						public boolean checkPreHier_pop(MyStack trg_instance){
							
								 boolean myPre = checkPre_pop( trg_instance );
								 boolean hierarchy  = (true);
								
								if (!hierarchy || myPre)
									 return myPre; 
								else
									 return false;
								}public boolean checkPostHier_pop(MyStack trg_instance, boolean last, int result){
									
								boolean postResult = checkPost_pop( trg_instance, result);
								if (!last || postResult){
									 return (true);
								
							}else 
								return false;
							}
							
							
							
							
							
							
							
							
							}