Select your answer and click the button below:    
Question3:  
  Card1 = ♣; S = <♠, ♥>;  
 

Operation PushCard (restores Card1: Card;
                                    updates S:Stack);
       ensures: S = Card1 o #S;

 
 
  After PushCard executes the values are:
   
  Card1 = ♠, S = <♣, ♠, ♥>;
Card1 is unknown, S = <♣, ♠, ♥>
Card1 = <♣>, S is unknown;
Card1 = <♣>, S = <♣, ♠, ♥>;