Property 8: FLAVERS QRE

Refinement: No artist attempts to register for event e1 when the size of the array used to store artists registered for e1 is equal to 2.

Pattern: generic check for violation.

Note: This requires the Ada source code to be modified by annotating the code with the violating predicate at any point where the array bound could be violated. See the modified Ada source code.

FLAVERS QRE:

for events {{e1_list_out_of_bounds}}

show no executions satisfy

.*;
{e1_list_out_of_bounds};
.*

Constraints used to verify this property:

• Counter constraint e1_size 0 2
• Enumerated constraint e1_list_1 disp.a_id_type disp_spec a1 a2
• Enumerated constraint e1_list_2 disp.a_id_type disp_spec a1 a2
• Task constraint disp.dispatcher

Up to Property 8: Size of registration list does not exceed 2

Forward to Property 9: FLAVERS

Back to Property 7: FLAVERS