CS 260r 2017 L13: IronFleet (3/8)
The Verdi key-value store specification uses per-key traces (page 364 of Verdi), whereas the IronKV key-value store specification uses a transition relation on an abstract hash-table state (Figure 11 on page 10 of IronFleet). Contrast these approaches.
Question 2 (optional but recommended)
The Verdi key-value store implementation at
supports five operations, get, put, delete, compare-and-swap, and compare-and-delete. Now consider the “high-level spec for IronKV” in Figure 11. Write a new version of this spec that supports at least one additional operation from VarD. (NB: In Dafny, the “::” operator means “such that,” not “cons.”)
Never submit passwords through Google Forms.
This form was created inside of Google Apps for Harvard.
Terms of Service