Action from Assertion meeting 3/21/02

Subject: Action from Assertion meeting 3/21/02
From: Peter Flake (flake@co-design.com)
Date: Thu Mar 28 2002 - 06:53:56 PST

At 03:09 PM 3/21/02 -0500, Tom Fitzpatrick wrote:
Erich to write a description of how to specify that a sequence cannot be
empty.

Peter to provide a new example for sequence repetition.
Here is my proposed amendment.

More Expression Sequences
A number of steps can be skipped either by writing expressions which are always true:
        assert  (a;1;1;c) // two steps between a and c

or by using the notation [n] to count the number of steps:
        assert  (a;[2];c); // two steps between a and c
        assert  (a;[1];[1];c)  // two steps between a and c

Note that in [n], the n must be a non-negative literal or constant expression. [0]; has no effect.  A variable number of steps can be indicated by [min:max], where the minimum can be zero.

If an expression  must be repeated a defined number of times, this can be expressed with a trailing *[n]. If it can be repeated a minimum or maximum number of times, this can be expressed with a trailing *[min : max].  These repetition counts must also be literals or constant expressions:
        assert  ( (a; b)*[5] ); // a;b;a;b;a;b;a;b;a;b
        assert  (a*[0:3];b;c); // (a;b) or (a;b;a;b)

Note that (a*[0:3];b;c) is equivalent to (b;c) or (a;b;c) or (a;a;b;c) or (a;a;a;b;c).  This means that a sequence a;ab;a;b;c; will pass.  The expression sequence is not equivalent to ((a && !b)* [0:3];b;c), which would fail the same sequence.

Also note that the sequence should not terminate with a variable number of steps or a variable repetition count, since the pass statement is executed at the lowest number.  The sequence must never be empty.

Peter.

This archive was generated by hypermail 2b28 : Thu Mar 28 2002 - 06:49:40 PST