Bounded_Stack : module body is
Stack : module body is
type Stack_Value is array (General_Index_Value range 1 .. Max_Size) : Element;
Top : General_Count_Value is 0;
Value : Stack_Value;
Push : procedure body (Item : in Element) is
null;
Push : begin
Top <- Top + 1;
Value (Top) <- Item;
Push : exception
when others =>
raise;
Push : end;
Pop : function body return Element is
null;
Pop : begin
Top <- Top - 1;
return Value (Top + 1);
Pop : exception
when others =>
raise;
Pop : end;
Length : function body return General_Count_Value is
null;
Length : begin
return Top;
Length : exception
when others =>
raise;
Length : end;
Is_Empty : function body return Boolean is
null;
Is_Empty : begin
return Top = 0;
Is_Empty : exception
when others =>
raise;
Is_Empty : end;
Is_Full : function body return Boolean is
null;
Is_Full : begin
return Top = Max_Size;
Is_Full : exception
when others =>
raise;
Is_Full : end;
Stack : end;
Bounded_Stack : end;
None of these operations can raise an exception that can be handled in the operation's exception handler. The preconditions for Push and Pop are evaluated before execution gets to the elaboration of the subprograms' declarative regions, ensuring that Top has a value suitable for the operations performed on it, and the others have innocuous return expressions that cannot raise an exception (except Memory_Exhausted, which anything may raise).
No comments:
Post a Comment