Is a formal specification complete ?

- Does it fully-define an actual implementation (this is overly restrictive) ?
- Does it exactly prescribe all allowable, observable behaviours ?

By `formal' we mean a machine-readable description of what is correct
or incorrect behaviour. A **complete** specification might describe all allowable
behaviours and prohibit all remaining behaviours, but most formal definitions
today are not complete in this sense. For instance, a definition that consists of
of a list of safety assertions and a few liveness assertions might still allow all
sorts of behaviours that the designer knows are wrong. He can go on adding
more assertions, but when does he stop ?

One might define a 'complete specification' as one that describes all observable behaviours. Such a specification does not restrict or prescribe the internal implementation in black box terms since this is not observable.

When testing an IP block, can we compute coverage somehow: e.g. What percentage of rule disjuncts held as dominators (on their own) ?

Or, e.g. What (inverse log) percentage of reachable state space was spanned?

There are no well-accepted coverage metrics for formal specifications. We could measure what percentage of rule disjuncts held as dominators (on their own) ? There is no clear definition of 100 percent coverage.

(C) 2008-10, DJ Greaves, University of Cambridge, Computer Laboratory.