Windows 7 Bart De Smet: LINQ to Z3

News

Extraordinary Robot
Robot
Bart De Smet is one of the highly talented software engineers on Erik Meijer's team and the chief architect of the LINQ to Anything dream. You should watch his excellent PDC10 session on this topic.As you learned on Channel 9 Live's PDC10 conversation with Wolfram Schulte and Erik Meijer, Z3 is a theorem prover (the fastest in the world, in fact). Z3 is one of several advanced software engineering technologies coming out of MSR's RiSE team.

A while ago, Bart implemented a LINQ to Z3 library and I've wanted to dig into this with him for some time. Recently, I got the chance to do just that and it makes for an excellent episode of Going Deep.

Bart writes in his initial post on the LINQ to Z3 project:

With LINQ to Z3 my goal is to abstract away from the low-level Z3 APIs and provide nice syntax with rich static typing support on top of it. The basic idea is the following:

  • Define the “shape” of a theorem, e.g. what symbolic names (and their types) to use;
  • Express constraints over those symbolic names using LINQ syntax (more specifically the where keyword);
  • Ask the resulting object for a solution, resulting in an instance of the “shape” type specified at the start.
An example of LINQ to Z3:


var theorem = from t in ctx.NewTheorem() where t.X1 - t.X2 >= 1 where t.X1 - t.X2
 
Back
Top