• bearophile (4/11) May 31 2014 It seems possible to integrate Z3 with D contract programming.

"bearophile" <bearophileHUGS lycos.com> writes:

https://github.com/tomprimozic/type-systems/tree/master/refined_types

The implementation of a refined type-checker is actually very 
straightforward and turned out to be much simpler than I 
expected. Essentially, program expressions and contracts on 
function parameters and return types are converted into a series 
of mathematical formulas and logical statements, the validity of 
which is then assessed using an external automated theorem 
prover Z3.<

It seems possible to integrate Z3 with D contract programming.

Bye,
bearophile