Section 6 of base-02 defines a specific order for the steps in the
verification process. The last sentence of section 6 says, "Verifiers
MUST apply the following steps in the order listed."
I think this is too prescriptive of the verification process. Later on,
it does say that some of the steps
There's some place in the draft where it says "these steps must be
performed such that the semantics are identical to processing them in
this order" --- i.e., it makes the sequential nature be to define
semantics, not to implement the code. I think that's probably
appropriate here as well.
e
