search

informalsystems / vdd

Verification-Driven Development
21 stars 0 forks source link

Correct description of implementation tagging #20

Closed shonfeder closed 3 years ago

shonfeder commented 3 years ago

I think we initially missed a detail of the spec. As per TRC-IMPL.1::PREFIX.1, an implementation unit is to be tagged with it's own pipe-designated tag that adds a suffix.

This is important for two reasons:

  1. It makes tagging implementation units trivial, in that we don't need to introduce new syntax (such as the ## Implements header I proposed elsewhere).
  2. It provides a unique tag for each implementation unit, which is critical for when we decompose a spec into many smaller implementation aspects, and for allowing unique reference from verification units, or other implementation units (e.g., when using a reference implementation as a spec).