search

informalsystems / vdd

Verification-Driven Development
21 stars 0 forks source link

Linkify traceability spec #22

Closed shonfeder closed 3 years ago

shonfeder commented 3 years ago

This adds links and anchors to the traceability spec (generated with themis-tracer linkify).

The diff is unfortunately long, but it's just because of reformatting for line wrapping. The only changes here are:

  1. Manually removed the unnecessary ** around unit refs.
  2. Programmatically ran linkification to provide anchors for each unit def and links for each unit reference (I also had one touch up, since tracer doesn't currently support the new tag synonymy links).

Rendered file is here: https://github.com/informalsystems/vdd/blob/3005154794b71e84ab6f1e43c2b1453205d86a25/traceability/traceability.md

shonfeder commented 3 years ago

Synonymy is not introduced in this pr. See #21 for more context.

As indicated in the spec, the motivation for synonym is to account for cases when "a logical unit implements multiple units from a higher level". That logical unit itself demonstrates a case of this.

Concretely, the kind of example that motivated this was when implementing the function to add logical units for the tracer tool. It satisfies both TRC-UNIQ.1::DUPS.1 (because we guard against dups when adding tags to the database) and TRC-GITHUB-REF.1::IMPL.1 (because we record the location of tags when we add them to the database). Without something like synonymy, I don't know how we'll deal with these kinds of cases.

All that said, I'd rather not have the additional complexity, either in parsing or in graph of dependencies. Can you think of a way this can be avoided? Is my thinking around the likelihood of one unit implementing multiple requirements wrong? Should that be impossible? If not, is there a better way to address this scenario?