Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Facility ATeam_Assignment3_1C;
- uses Integer_Template, Preemptable_Queue_Template;
- Facility Queue_Fac is Preemptable_Queue_Template(Integer, 3)
- realized by Master_Circular_Array_Realiz;
- 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 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 |Q| >= 1;
- ensures #Q = Q;
- Procedure
- Var I: Integer;
- I := 1;
- 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: P_Queue;
- Var I: Integer;
- Read_Queue(Q);
- Copy_Front(Q, I);
- Write_Line(I);
- Rotate(Q);
- Write_Queue(Q);
- end Main;
- end ATeam_Assignment3_1C;
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
