Roberto Guanciale

I would love to have touch feedback, but I hate phone haptic vibrations. I'm really thinking of buying a new screen protector and engrave the keyboard diagonals :)

I would be happy to get some help

I had the same problem executing the S2JSPluginRunner from command line even if I set the classpath. Changing line of S2JSPluginRunner as follows solves the problem for me - settings.classpath.tryToSet(List("bin"))...

Also add to the wiki the simpset that we use often

For the tutorial we used a simple approach. We take an additional list of labels, for which we use `false` as precondition. This approach is sound because `{false}l->ls{Q}` always holds....

We could generalize this approach, by allowing the `WP` procedure to take a list of initial contracts: `WP(l, ls, thms, Q)`, where each theorem in `thms` is a contract `{P}l1->ls{Q}`.

An alternative approach is to change the definition of the triple, allowing to specify different postcondition for different exit points. E.g `{P}l1[l2->Q, l3->Q', etc]`. This approach could make sense for...

For Add memory should be possible one button solution plus bsl