Untitled

Rafael09ED

Nov 29th, 2018

519

Never

Add comment

Not a member of Pastebin yet? Sign Up, it unlocks many cool features!

text 3.40 KB | None | 0 0

raw download clone embed print report

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;

Add Comment

Please, Sign In to add comment