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.


for events {{e1_list_out_of_bounds}}

show no executions satisfy


Constraints used to verify this property:

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

Forward to Property 9: FLAVERS

Back to Property 7: FLAVERS