www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Refinement types in OCaML


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
May 31 2014