Advertisement
Rafael09ED

Untitled

Nov 29th, 2018
520
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 3.40 KB | None | 0 0
  1. Facility ATeam_Assignment3;
  2. uses Integer_Template, Preemptable_Queue_Template;
  3.  
  4. Facility Queue_Fac is Preemptable_Queue_Template(Integer, 3)
  5. realized by Master_Circular_Array_Realiz
  6. enhanced by Inverting_Capability
  7. realized by Recursive_Inverting_Realiz;
  8.  
  9. Operation Do_Nothing (restores Q: P_Queue);
  10. ensures Q = #Q;
  11. Procedure
  12. Var Temp_Queue: P_Queue;
  13. Var I, J: Integer;
  14. While(1 <= Length(Q))
  15. maintaining 0 <= |Q|;
  16. decreasing |Q|;
  17. do
  18. Dequeue(I, Q);
  19. If(1 <= Rem_Capacity(Temp_Queue)) then
  20. Enqueue(I, Temp_Queue);
  21. end;
  22. end;
  23.  
  24. While(1 <= Length(Temp_Queue))
  25. maintaining 0 <= |Temp_Queue|;
  26. decreasing |Temp_Queue|;
  27. do
  28. Dequeue(I, Temp_Queue);
  29. If(1 <= Rem_Capacity(Q)) then
  30. Enqueue(I, Q);
  31. end;
  32. end;
  33.  
  34. end Do_Nothing;
  35.  
  36. Operation Do_Nothing_1 (restores Q: P_Queue);
  37. --requires |Q| = 2;
  38. Procedure
  39. Var temp, I, J: Integer;
  40.  
  41. If (Length(Q) = 2) then
  42. Dequeue(I, Q);
  43. Dequeue(J, Q);
  44. Enqueue(I, Q);
  45. Enqueue(J, Q);
  46. end;
  47. end Do_Nothing_1;
  48.  
  49. Operation Read_Queue(replaces Q: P_Queue);
  50. Procedure
  51. Var I: Integer;
  52.  
  53. Clear(Q);
  54. While ( 1 <= Rem_Capacity(Q) )
  55. decreasing 3 -|Q|;
  56. do
  57. Read(I);
  58. Enqueue(I, Q);
  59. end;
  60. end Read_Queue;
  61.  
  62. Operation Write_Queue(clears Q: P_Queue);
  63. Procedure
  64. Var I: Integer;
  65.  
  66. While (Length(Q) > 0)
  67. decreasing |Q|;
  68. do
  69. Dequeue(I, Q);
  70. Write_Line(I);
  71. end;
  72. end Write_Queue;
  73.  
  74. Operation Copy_Queue(restores Q: P_Queue; replaces Q_Copy: P_Queue);
  75. ensures Q_Copy = Q;
  76.  
  77. Procedure
  78. Var I: Integer;
  79. Var I_c: Integer;
  80.  
  81. While (Length(Q_Copy) < Length(Q))
  82. decreasing (|Q| - |Q_Copy|);
  83. do
  84. Dequeue(I, Q);
  85. I_c := I;
  86. Enqueue(I, Q);
  87. Enqueue(I_c, Q_Copy);
  88. end;
  89. end Copy_Queue;
  90.  
  91. Operation Rotate (updates Q: P_Queue);
  92. requires 1 <= |Q|;
  93. ensures Q = Prt_Btwn(1, |#Q|, #Q) o Prt_Btwn(0, 1, #Q);
  94. Procedure
  95. Var I: Integer;
  96.  
  97. Dequeue(I, Q);
  98. Enqueue(I, Q);
  99. end Rotate;
  100.  
  101. Operation Copy_Front (restores Q: P_Queue; replaces Front: Integer);
  102. requires 1 <= |Q|;
  103. ensures <Front> = Prt_Btwn(0, 1, Q);
  104. Procedure
  105. Var I: Integer;
  106.  
  107. Dequeue(I, Q);
  108. Front := I;
  109. Inject(I, Q);
  110. end Copy_Front;
  111.  
  112. Operation Do_Nothing_with_Swap_Last_Entry (updates Q:P_Queue);
  113. requires 1 <= |Q|;
  114. Procedure
  115. Var I: Integer;
  116.  
  117. Swap_Last_Entry(I, Q);
  118. Swap_Last_Entry(I, Q);
  119. end Do_Nothing_with_Swap_Last_Entry;
  120. --- make proper use of the Swap_Last_Entry operation in this code
  121.  
  122. Operation Main();
  123. Procedure
  124. Var Q, Q_Copy: P_Queue;
  125. Var I: Integer;
  126. Read_Queue(Q);
  127. --Copy_Front(Q, I);
  128. Write_Line(I);
  129. --Rotate(Q);
  130. Write_Queue(Q);
  131. --Copy_Queue(Q, Q_Copy);
  132. Invert(Q);
  133.  
  134. end Main;
  135.  
  136. end ATeam_Assignment3;
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement