Property 8: INCA Query

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 assertion violations.

Note: This requires the SEDL code to be modified by inserting appropriate assert statements at the points where the array bound could be violated. See the modified SEDL source code.

INCA Query:

(defquery "p08a" "nofair"
  (omega-star-less
    (sequence
      (interval
        :initial t
        :constraints '((>= "exception(dispatcher;assert)" 1))))))

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

Forward to Property 9: INCA

Back to Property 7: INCA