Our spec graph is a digraph from the most general, high-level requirements down
to refined, increasingly specified implementations. However, at some point, the
units need to stop branching, and we need to terminate the chain at
implementations of the requirements and verifications of their satisfaction.
We need a syntax or convention that will let us recognize when such satisfaction
has been reached.
These terminal nodes should include "views" in the sense of justifications that
an implementation satisfies the indicated specs (see #29).
Our spec graph is a digraph from the most general, high-level requirements down to refined, increasingly specified implementations. However, at some point, the units need to stop branching, and we need to terminate the chain at implementations of the requirements and verifications of their satisfaction.
We need a syntax or convention that will let us recognize when such satisfaction has been reached.
These terminal nodes should include "views" in the sense of justifications that an implementation satisfies the indicated specs (see #29).