           *******************************************************
                       Semantic Analysis of SPARK Text
                             Examiner GPL Edition

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


               procedure Task_Limit.Task_Count_Type.Increment




For path(s) from start to run-time check associated with statement of line 42:

procedure_increment_1.
H1:    task_count_type__task_count >= 0 .
H2:    task_count_type__task_count <= max_tasks .
H3:    task_count_type__task_count >= task_count_subtype__first .
H4:    task_count_type__task_count <= task_count_subtype__last .
H5:    task_count_type__task_count < max_tasks .
        ->
C1:    task_count_type__task_count + 1 >= 
           task_count_subtype__first .
C2:    task_count_type__task_count + 1 <= 
           task_count_subtype__last .
 

For path(s) from start to finish:

procedure_increment_2.
H1:    task_count_type__task_count >= 0 .
H2:    task_count_type__task_count <= max_tasks .
H3:    task_count_type__task_count >= task_count_subtype__first .
H4:    task_count_type__task_count <= task_count_subtype__last .
H5:    task_count_type__task_count < max_tasks .
H6:    task_count_type__task_count + 1 >= 
           task_count_subtype__first .
H7:    task_count_type__task_count + 1 <= 
           task_count_subtype__last .
        ->
C1:    task_count_type__task_count + 1 >= 0 .
C2:    task_count_type__task_count + 1 <= max_tasks .
C3:    (task_count_type__task_count = max_tasks) -> ((
           task_count_type__task_count + 1 = 
           task_count_type__task_count) and (true = false)) .
C4:    (task_count_type__task_count < max_tasks) -> ((
           task_count_type__task_count + 1 = 
           task_count_type__task_count + 1) and true) .
 

procedure_increment_3.
H1:    task_count_type__task_count >= 0 .
H2:    task_count_type__task_count <= max_tasks .
H3:    task_count_type__task_count >= task_count_subtype__first .
H4:    task_count_type__task_count <= task_count_subtype__last .
H5:    not (task_count_type__task_count < max_tasks) .
        ->
C1:    task_count_type__task_count >= 0 .
C2:    task_count_type__task_count <= max_tasks .
C3:    (task_count_type__task_count = max_tasks) -> ((
           task_count_type__task_count = 
           task_count_type__task_count) and (false = false)) .
C4:    (task_count_type__task_count < max_tasks) -> ((
           task_count_type__task_count = 
           task_count_type__task_count + 1) and false) .
 

For checks of refinement integrity: 

procedure_increment_4.
H1:    task_count_type__task_count >= task_count_subtype__first .
H2:    task_count_type__task_count <= task_count_subtype__last .
        ->
C1:    task_count_type__task_count >= 0 .
C2:    task_count_type__task_count <= max_tasks .
 

procedure_increment_5.
*** true .          /* trivially true VC removed by Examiner */


