           *******************************************************
                            Listing of SPARK Text
                             Examiner GPL Edition

           *******************************************************


Line
      ----------------------------------------------------------------
      -- 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;

+++        Flow analysis of subprogram Increment performed 
           (information-flow mode): no errors found.

      
            ---------------
            -- 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;

+++        Flow analysis of subprogram Decrement performed 
           (information-flow mode): no errors found.

      
         end Task_Count_Type;
      
      end Task_Limit;

Note: Flow analysis mode is automatic


--End of file--------------------------------------------------
