Have you ever thought how exciting verification tools are? How do you prove the correctness of a program? Of course, the green tests bring some confidence… but we all know it’s not a proof.
Just look at Pex, it definitely can’t leave anybody cold (recommendation: skip this step for now, it was a trap).
But this story is not about Pex, but what powers it - Z3, an efficient SMT solver from Microsoft Research. You may ask why you should care (at least I always do when looking at something new - a tool/language/app/whatever), the answer is simple - because we want the proof, not only a bunch of valid inputs. The work made me a bit paranoid to this point - it takes more time, but the shining correctness allows you not to worry about how much customers can lose just because someone forgot about a not-likely-to-happen workflow, like an unexpected negative number from nowhere -> power -> NaN (surprise, surprise!).
Z3 is supported on Windows, OSX, Linux and FreeBSD and has an extensive API: C, C++, OCaml, .NET languages, Python, Java.
Z3 + Mono
The standard Z3 distrubution for OSX comes with x64 binaries, but to get it working with Mono we need to compile it ourselves with x86 architecture.
1. Download the sources here.
2. Open the folder and generate the makefiles.
3. We’re interested in
config.mk file. By default the result architecture is x86_x64, that’s where the compiler flags help:
Update: according to the Yu’s comment you might need to replace the option
4. Just make it 1. The recent Z3 versions require a little change as compiler gives
typename outside of template error, I just removed
5. Check the architecture
6. cd to
z3/src/api/dotnet folder and compile Microsoft.Z3.csproj with Mono/.NET 4.0 as a target framework 2. Also you’d need to add a config file to map
libz3.dll to our fresh native
Now we are ready to try it!
Let’s start with a simple script using official Z3 API, the C# version of examples below can be found in Z3 repository. There’s also a nice set of F# examples - I couldn’t leave it just in comments - Z3Fs, a DSL to solve SMT problems by @dungpa.
For simplicity we assume that Microsoft.Z3.dll, config and libz3.dylib are in the script’s folder.
Prove that x = y implies g(x) = g(y).
Well, it’s a pain to write all those
ctx.Mk*. That’s where F# quotations come to hand. Some papers and slides mention Z3 support for quotations, though they seem to be a bit outdated - haven’t seen anything similar in the sources. Here is an example of what it can look like.
Simplify expression “x + (y - (x + z))”
Looks much better, doesn’t it?
Next time: bringing another f-language to mono…