The Verification Corner - Specifications in Action with Spec#

Play The Verification Corner - Specifications in Action with Spec#

The Discussion

  • User profile image

    That's a pretty impressive example. It makes clear how many possible bugs specifications can catch: a lot. It also makes me quite envious of Spec#. Hopefully these features will be incorporated into C# at some point in time; we do have Code Contracts for .Net but this syntax is so much better. It would also be very nice to be able to assign invariants to primitive type aliases, e.g.


    alias nat = int where nat >= 1;


    Maybe there's not that many use-cases for that feature though.


    Non-nullness annotations is another very hot feature.


    Also, since LINQ to Objects uses Dispose (as in IEnumerator extends IDisposable; the sole purpose of which is IO cleanup) can we then consider LINQ to Objects as impure and therefore not suitable for specifications?

  • User profile image

    Very nice, but I'd like to see the full postcondition for NextChunk. Perhaps, in your next episode, you could give an example of a postcondition containing, say, a quantified expression.

Add Your 2 Cents