Dynamic verification traversal strategies

1. A computer-implemented method of implementing a traversal strategy as part of a dynamic verification, comprising:

initializing a non-deterministic automaton (NDA) traversal mechanism having (1) a strategy push-down stack (strategy PDS) that holds traversal strategy pointers and (2) an object push-down stack (object PDS) that holds object pointers;

pushing a traversal strategy object pointer onto the strategy PDS, wherein the traversal strategy object pointer points to a traversal strategy object;

popping a current object pointer from the object PDS; and

determining whether the current object pointer points to a terminal object.

2. The computer-implemented method of claim 1 further comprising, if the current object pointer is determined to point to the terminal object, processing the terminal object, wherein the processing comprises:

comparing the current object pointer to a target terminal pointer in the traversal strategy object, wherein the target terminal pointer points to the terminal object; and

if the comparing results in the current object pointer matching the target terminal pointer, popping the traversal strategy object pointer off the strategy PDS, deleting the traversal strategy object, and calling a corresponding action routine via an action routine pointer stored in the terminal object.

3. The computer-implemented method of claim 1 further comprising, if the current object pointer is determined to point to the terminal object, processing the terminal object, wherein the processing comprises:

comparing the current object pointer to a target terminal pointer in the traversal strategy object, wherein the target terminal pointer points to the terminal object; and

if the comparing results in the current object pointer not matching the target terminal pointer, providing a notification of an illegal force.

4. The computer-implemented method of claim 1 further comprising, if the current object pointer is determined to point to a sequence object having a list of expression object pointers, pushing the expression object pointers onto the object PDS.

5. The computer-implemented method of claim 1 further comprising, if the current object pointer is determined to point to an alternative set object having a list of alternative object pointers, processing the alternative set object, wherein the processing comprises:

forming a first subset of the alternative object pointers, wherein the alternative object pointers in the first subset each point to an alternative object having a zero weight;

forming a second subset of the alternative object pointers, wherein the alternative object pointers in the second subset each point to an alternative object having a zero weight; and

if the first subset is non-empty, making a weighted pseudo-random selection of one of the alternative object pointers in the first subset and pushing the selected alternative object pointer onto the object PDS.

6. The computer-implemented method of claim 1 further comprising, if the current object pointer is determined to point to an alternative set object having a list of alternative object pointers, processing the alternative set object, wherein the processing comprises:

forming a first subset of the alternative object pointers, wherein the alternative object pointers in the first subset each point to an alternative object having a zero weight;

forming a second subset of the alternative object pointers, wherein the alternative object pointers in the second subset each point to an alternative object having a zero weight; and

if the first subset is empty, making a non-weighted pseudo-random selection of one of the alternative object pointers in the second subset and pushing the selected alternative object pointer onto the object PDS.

7. The computer-implemented method of claim 1 further comprising, if the current object pointer is determined to point to an alternative object having at least one expression object pointer, processing the alternative object, wherein the processing comprises pushing the at least one expression object pointer onto the object PDS.

8. The computer-implemented method of claim 1 further comprising, if the current object pointer is determined to point to a repeat object, processing the repeat object, wherein the processing comprises:

creating a repetition control object having a pointer to the repeat object, a repetition counter, and a repetition target; and

pushing a pointer to the repetition control object onto the object PDS.

9. The computer-implemented method of claim 1 further comprising, if the current object pointer is determined to point to a repetition control object having a repetition counter and at least one expression pointer, processing the repetition control object, wherein the processing comprises:

comparing the repetition counter to a predetermined maximum value; and

if the comparing results in determining that the repetition counter is less than the predetermined maximum value, incrementing the repetition counter by one, pushing the current object pointer onto the object PDS, and pushing the at least one expression pointer onto the object PDS.

10. The computer-implemented method of claim 1 further comprising, if the current object pointer is determined to point to a repetition control object having a repetition counter and at least one expression pointer, processing the repetition control object, wherein the processing comprises:

comparing the repetition counter to a predetermined maximum value; and

if the comparing results in determining that the repetition counter is not less than the predetermined maximum value, deleting the repetition control object.

11. The computer-implemented method of claim 9 further comprising comparing the repetition counter to a predetermined minimum value and, if the comparing results in determining that the repetition counter is not less than the predetermined minimum value, deleting the repetition control object.

12. The computer-implemented method of claim 1 , wherein the traversal strategy object comprises at least one of a force traversal strategy (FTS) object and a skip traversal strategy (STS) object, and the traversal strategy object pointer comprises at least one of a FTS object pointer and a STS object pointer.

13. An apparatus, comprising:

a non-deterministic automaton (NDA) traversal mechanism comprising:

a strategy push-down stack (strategy PDS) operable to hold at least one traversal strategy pointer; and

an object push-down stack (object PDS) operable to hold at least one object pointer;

a first traversal strategy object pointer pushed onto the strategy PDS, the first traversal strategy object pointer pointing to a traversal strategy object;

a current object pointer popped off the object PDS; and

a current object pointer determining mechanism operable to determine whether the current object pointer points to a terminal object.

14. One or more computer-readable media having stored thereon computer-executable instructions for performing a method comprising:

initializing a non-deterministic automaton (NDA) traversal mechanism having (1) a strategy push-down stack (strategy PDS) that holds traversal strategy pointers and (2) an object push-down stack (object PDS) that holds object pointers;

pushing a traversal strategy object pointer onto the strategy PDS, wherein the traversal strategy object pointer points to a traversal strategy object;

popping a current object pointer from the object PDS; and

determining whether the current object pointer points to a terminal object.

15. The one or more computer-readable media of claim 14 , the method further comprising, if the current object pointer is determined to point to the terminal object, processing the terminal object, wherein the processing comprises:

comparing the current object pointer to a target terminal pointer in the traversal strategy object, wherein the target terminal pointer points to the terminal object; and

if the comparing results in the current object pointer matching the target terminal pointer, popping the traversal strategy object pointer off the strategy PDS, deleting the traversal strategy object, and calling a corresponding action routine via an action routine pointer stored in the terminal object.

16. The one or more computer-readable media of claim 14 , the method further comprising, if the current object pointer is determined to point to a sequence object having a list of expression object pointers, pushing the expression object pointers onto the object PDS.

17. The one or more computer-readable media of claim 14 , the method further comprising, if the current object pointer is determined to point to an alternative set object having a list of alternative object pointers, processing the alternative set object, wherein the processing comprises:

forming a first subset of the alternative object pointers, wherein the alternative object pointers in the first subset each point to an alternative object having a zero weight;

forming a second subset of the alternative object pointers, wherein the alternative object pointers in the second subset each point to an alternative object having a zero weight;

making a weighted pseudo-random selection of at least one of the alternative object pointers in at least one of the first subset and the second subset; and

pushing the selected alternative object pointer onto the object PDS.

18. The one or more computer-readable media of claim 14 , the method further comprising, if the current object pointer is determined to point to an alternative object having at least one expression object pointer, processing the alternative object, wherein the processing comprises pushing the at least one expression object pointer onto the object PDS.

19. The one or more computer-readable media of claim 14 , the method further comprising, if the current object pointer is determined to point to a repeat object, processing the repeat object, wherein the processing comprises:

creating a repetition control object having a pointer to the repeat object, a repetition counter, and a repetition target; and

pushing a pointer to the repetition control object onto the object PDS.

20. The one or more computer-readable media of claim 14 , the method further comprising, if the current object pointer is determined to point to a repetition control object having a repetition counter and at least one expression pointer, processing the repetition control object, wherein the processing comprises comparing the repetition counter to at least one of a predetermined maximum value and a predetermined minimum value.