Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Facility ATeam_Assignment3;
- uses Integer_Template, Preemptable_Queue_Template;
- Facility Queue_Fac is Preemptable_Queue_Template(Integer, 3)
- realized by Master_Circular_Array_Realiz
- enhanced by Inverting_Capability
- realized by Recursive_Inverting_Realiz;
- Operation Do_Nothing (restores Q: P_Queue);
- ensures Q = #Q;
- Procedure
- Var Temp_Queue: P_Queue;
- Var I, J: Integer;
- While(1 <= Length(Q))
- maintaining 0 <= |Q|;
- decreasing |Q|;
- do
- Dequeue(I, Q);
- If(1 <= Rem_Capacity(Temp_Queue)) then
- Enqueue(I, Temp_Queue);
- end;
- end;
- While(1 <= Length(Temp_Queue))
- maintaining 0 <= |Temp_Queue|;
- decreasing |Temp_Queue|;
- do
- Dequeue(I, Temp_Queue);
- If(1 <= Rem_Capacity(Q)) then
- Enqueue(I, Q);
- end;
- end;
- end Do_Nothing;
- Operation Do_Nothing_1 (restores Q: P_Queue);
- --requires |Q| = 2;
- Procedure
- Var temp, I, J: Integer;
- If (Length(Q) = 2) then
- Dequeue(I, Q);
- Dequeue(J, Q);
- Enqueue(I, Q);
- Enqueue(J, Q);
- end;
- end Do_Nothing_1;
- Operation Read_Queue(replaces Q: P_Queue);
- Procedure
- Var I: Integer;
- Clear(Q);
- While ( 1 <= Rem_Capacity(Q) )
- decreasing 3 -|Q|;
- do
- Read(I);
- Enqueue(I, Q);
- end;
- end Read_Queue;
- Operation Write_Queue(clears Q: P_Queue);
- Procedure
- Var I: Integer;
- While (Length(Q) > 0)
- decreasing |Q|;
- do
- Dequeue(I, Q);
- Write_Line(I);
- end;
- end Write_Queue;
- Operation Copy_Queue(restores Q: P_Queue; replaces Q_Copy: P_Queue);
- ensures Q_Copy = Q;
- Procedure
- Var I: Integer;
- Var I_c: Integer;
- While (Length(Q_Copy) < Length(Q))
- decreasing (|Q| - |Q_Copy|);
- do
- Dequeue(I, Q);
- I_c := I;
- Enqueue(I, Q);
- Enqueue(I_c, Q_Copy);
- end;
- end Copy_Queue;
- Operation Rotate (updates Q: P_Queue);
- requires 1 <= |Q|;
- ensures Q = Prt_Btwn(1, |#Q|, #Q) o Prt_Btwn(0, 1, #Q);
- Procedure
- Var I: Integer;
- Dequeue(I, Q);
- Enqueue(I, Q);
- end Rotate;
- Operation Copy_Front (restores Q: P_Queue; replaces Front: Integer);
- requires 1 <= |Q|;
- ensures <Front> = Prt_Btwn(0, 1, Q);
- Procedure
- Var I: Integer;
- Dequeue(I, Q);
- Front := I;
- Inject(I, Q);
- end Copy_Front;
- Operation Do_Nothing_with_Swap_Last_Entry (updates Q:P_Queue);
- requires 1 <= |Q|;
- Procedure
- Var I: Integer;
- Swap_Last_Entry(I, Q);
- Swap_Last_Entry(I, Q);
- end Do_Nothing_with_Swap_Last_Entry;
- --- make proper use of the Swap_Last_Entry operation in this code
- Operation Main();
- Procedure
- Var Q, Q_Copy: P_Queue;
- Var I: Integer;
- Read_Queue(Q);
- --Copy_Front(Q, I);
- Write_Line(I);
- --Rotate(Q);
- Write_Queue(Q);
- --Copy_Queue(Q, Q_Copy);
- Invert(Q);
- end Main;
- end ATeam_Assignment3;
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement