** Next:** A very simple example
** Up:** Refinement verification
** Previous:** Decomposing large structures in
** Contents**

##

Case analysis

Suppose that we have a condition `p`, and we would like to show
that `p` holds true at all times. For any particular variable `x`, we could break the problem into cases. For each possible value of
`v` of `x`, we could show that condition `p` is true at
those times when `x = v`. Since at all times `x` must have one
of these values, we can infer that `p` must be true at all times.
SMV has a special construct to support this kind of case analysis. It
is especially useful for compositional verification, since for each
case we can use a different abstraction of the system, including
different components in the verification. This allows us to break
large verification problems into smaller ones.

The above described case analysis is expressed in SMV in the following way:

forall (v in TYPE)
subcase q[v] of p for x = v;

Now suppose that `p` is some temporal assertion `G cond`, where
`cond` is any boolean condition. The above declaration effectively
defines a collection of properties `q[v]`, as if we had written

forall (x in TYPE)
q[v] assert G (x=v -> cond);

That is, each `q[v]` asserts that `p` holds at those times
when `x = v`. Clearly, if `q[v]` holds for all values of `v`, then `p` holds. Thus, SMV is relieved of the obligation of
proving `p`, and instead separately proves all the cases of `q[v]`. Note that if `TYPE` is a scalarset type, we may in fact
have to prove only one case, since all the other cases are symmetric.

**Subsections**

** Next:** A very simple example
** Up:** Refinement verification
** Previous:** Decomposing large structures in
** Contents**
2003-01-07