Select your answer and click the button below:    
Question4:  
  MyCard = ♦; S = <♥, ♠, ♦, ♣>;  
 

Operation PopCard (replaces MyCard: Card;
                                 updates S: Stack);
       requires |S| > 0;
       ensures: MyCard o S = #S;
 

 
  After Pop executes the values are:
   
  MyCard = ♦, S = <♥, ♠, ♦, ♣ >;
MyCard is unknown, S = < ♠, ♦, ♣ >
MyCard = ♥, S is unknown;
MyCard = ♥, S = <♠, ♦, ♣>;