Abstract

We introduce a new tool employing the sketching synthesis technique in programs annotated with declarative contracts. While Sketch, the original sketching tool, reasons entirely on imperative code, Sketch# works on top of the full-fledged specification language Spec#. In such a language, high-level specifications in the form of pre- and postconditions annotate code, which can be formally verified using decision procedures. But once a given method's implementation is verified, there is no need to look inside its body again. An invocation of the method elsewhere simply implies its specified postcondition. The approach widens the scalability of the sketching technique, as reasoning can be done in a modular manner when specifications accompany implementations. This paper describes our implementation of Sketch# on top of Spec# and its program verifier Boogie. We also recount our experience applying the tool to aid optimistic parallel execution frameworks, where we used it to discover and verify operation inverses, commutativity conditions, and operational transformations for several data structures.