71 lines
2.4 KiB
Ada
71 lines
2.4 KiB
Ada
----------------------------------------------------------------
|
|
-- IRONSIDES - DNS SERVER
|
|
--
|
|
-- By: Martin C. Carlisle and Barry S. Fagin
|
|
-- Department of Computer Science
|
|
-- United States Air Force Academy
|
|
--
|
|
-- This is free software; you can redistribute it and/or
|
|
-- modify without restriction. We do ask that you please keep
|
|
-- the original author information, and clearly indicate if the
|
|
-- software has been modified.
|
|
--
|
|
-- This software is distributed in the hope that it will be useful,
|
|
-- but WITHOUT ANY WARRANTY; without even the implied warranty
|
|
-- of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
|
|
----------------------------------------------------------------
|
|
|
|
--with ada.text_io;
|
|
package body Task_Limit is
|
|
|
|
---------------------
|
|
-- Task_Count_Type --
|
|
---------------------
|
|
|
|
protected body Task_Count_Type is
|
|
|
|
---------------
|
|
-- Increment --
|
|
---------------
|
|
|
|
procedure Increment (Success : out Boolean)
|
|
--# global in out Task_Count;
|
|
--# derives Task_Count from * &
|
|
--# Success from Task_Count;
|
|
--# pre Task_Count >= 0 and Task_Count <= MAX_TASKS;
|
|
--# post Task_Count >= 0 and Task_Count <= MAX_TASKS and
|
|
--# (((Task_Count~ = MAX_TASKS) -> ((Task_Count = Task_Count~) and (Success=False))) and
|
|
--# ((Task_Count~ < MAX_TASKS) -> ((Task_Count = Task_Count~ + 1) and Success)));
|
|
is
|
|
begin
|
|
if Task_Count < MAX_TASKS then
|
|
Task_Count := Task_Count + 1;
|
|
--ada.Text_IO.put_line("increment : " & integer'image(task_count));
|
|
Success := True;
|
|
else
|
|
Success := False;
|
|
end if;
|
|
end Increment;
|
|
|
|
---------------
|
|
-- Decrement --
|
|
---------------
|
|
|
|
procedure Decrement
|
|
--# global in out Task_Count;
|
|
--# derives Task_Count from *;
|
|
--# pre Task_Count >= 0 and Task_Count <= MAX_TASKS;
|
|
--# post Task_Count >= 0 and Task_Count <= MAX_TASKS and
|
|
--# (Task_Count~ > 0 -> (Task_Count = Task_Count~ - 1)) and
|
|
--# (Task_Count~ = 0 -> (Task_Count = Task_Count~));
|
|
is
|
|
begin
|
|
if Task_Count > 0 then
|
|
Task_Count := Task_Count - 1;
|
|
end if;
|
|
end Decrement;
|
|
|
|
end Task_Count_Type;
|
|
|
|
end Task_Limit;
|