Welcome to part two! If you haven't already, check out part one, where we introduce DSCheck and share one of its uses in a naive counter implementation. This post will give you a behind-the-scenes look at how DSCheck works its magic, including the theory behind it and how to write a test for our naive counter implementation example. We’ll conclude by going a bit further, showing you how DSCheck can be used to check otherwise hard-to-prove properties in the Saturn library. How Does DSCheck W...
