There’s a gap between knowing how to write specifications and knowing how to write them well. Much of this gap is from the “small stuff”: all of the little tips, tricks, and traps that experts implicitly know but beginners rarely learn. Things like “the best way to represent nested state” or “how to debug a slow model.” This talk will be a general introduction to intermediate-level techniques. Topics will include:
Most topics will be applicable to both TLA+ and PlusCal, but some language-specific techniques will also be covered. Advanced specification topics such as partial specifications may be discussed if time permits.