Trigger Discovery

[DavePearce]

See dafny-lang/dafny#1544

The boogie backend for Whiley currently does not support trigger discovery. Its likely this is the reason that it cannot verify the std::array::copy<T>() function from https://github.com/Whiley/STD.wy

[RustanLeino]

A note: As described in "Trigger selection strategies to stabilize verifiers" (CAV 2016), trigger discovery seems best done at the source level (rather than at the level of Boogie or the SMT solver) because of (what the paper calls) parasitic terms. So, though there may not be code sharing, Whiley could use the same ideas (and could probably also copy-and-edit some code from here).

[DavePearce]

Thanks @RustanLeino, great --- I'll take a look at your trigger code! I did see that paper before, but I've been meaning to reread it. I'm trying to get my standard library to verify, and have only one function left. But, it needs a trigger to verify it and this is motivating me to investigate this now finally!!

[DavePearce]

This seems like another relevant paper:

Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers