To begin with, let's define our types:

scalarset BIT 0..7; typedef BYTE array BIT of boolean; ordset INDEX 0..;

Note that we defined `INDEX` as an ordset type, so we can prove
properties by induction over indices.

We begin with the original refinement specification. As in section 4.2.3, we encapsulate it in a module, so we can reuse it for both input and output:

module byte_intf(bytes){ bytes : array INDEX of BYTE; valid : boolean; idx : INDEX; data : BYTE; layer spec: if(valid) data := bytes[idx]; }

To specify ordering we simply introduce a counter `cnt` that
counts the number of bytes received thus far. If there is valid
data at the interface, we specify that the index of that data is
equal to `cnt`. Thus, add the following declarations
to module `byte_intf`:

cnt : INDEX; init(cnt) := 0; if(valid) next(cnt) := cnt + 1; ordered: assert G (valid -> idx = cnt);Note, we can include temporal properties, like the above property

module main(bytes,inp,out){ bytes : array INDEX of BYTE; input inp : byte_intf(bytes); output out : byte_intf(bytes); /* the abstract model */ next(bytes) := bytes; /* the implementation */ init(out.valid) := 0; next(out.valid) := inp.valid; next(out.data) := inp.data; next(out.idx) := inp.idx; }To prove the correctness of the data output (with respect to the refinement specification), we use the same proof as before - we split into cases based on the index of the output:

forall(i in INDEX) subcase spec_case[i] of out.data//spec for out.idx = i;

Note that anything that can be done with a scalarset can also be done with an ordset.

So much for the data correctness - the interesting part is the
correct ordering. For the proof of the ordering property, we're going
to use induction over the value of the counter `cnt`. The
intuition here is that, if the output index equals the counter when
the counter is `i`, then at the next valid output the counter and
index will both be one greater, and hence they will be equal for `cnt = i + 1`. This assumes, of course, that the input values are
ordered correctly. To verify this, we must first break the output
ordering property into cases based on the value of cnt:

forall(i in INDEX) subcase ord_case[i] of out.ordered for out.cnt = i;

Then, we prove case `i` using case `i-1` and the input ordering
property. We leave `inp.ordering` as an assumption:

forall(i in INDEX){ using ord_case[i-1], inp.ordered prove ord_case[i]; assume inp.ordered; }

Now, run this example,
and observe the properties pane. You'll notice that we now have two cases
of the property `out.data//spec_case[i]` to prove: `i = 0, 2`.
In fact, these two cases are isomorphic, but since `INDEX` is defined
as an ordset rather than a scalarset, SMV's type checking rules don't guarantee
this. Thus, SMV will effectively prove the same property twice. Fortunately,
each case takes only a fraction of a second.

Now observe that we also have two cases of `ord_case[i]` to prove.
Select, for example, property `ord_case[2]` from the properties pane
and observe the cone. You'll notice that each value of type `INDEX`
requires two boolean variables to encode it. This is because there are
four values in the reduced type: `i-1`, `i` and
two abstract values to represent the ranges `[0..i-1)` and `(i..infinity)`.
Notice also that there are no data values in the cone, since the indices
do not depend on the data. Thus, we have effectively separated the problem of
correct ordering from correct delivery of data.

Now, try `Prop|Verify all`. All the cases should be verified in less
than a second.

A note: for ordsets, a data type reduction may be specified, in lieu of SMV's default. The general form of the data type reduction for ordset types is:

TYPE -> { min..min+a, i-b..i+c, max-d..max};where