digitalmars.D.learn - Do assertions provide a mechanism for subtyping? If not are they
- Jonathan (26/26) Dec 29 2013 D allows inputs and outputs to have assertions placed on them.
- bearophile (6/8) Dec 29 2013 Currently D doesn't statically verify them. I have an enhancement
- Jonathan (2/6) Jan 01 2014 Is there a link available, so that I could see what is in the
- bearophile (5/7) Jan 01 2014 Yes, this is two thirds of my proposal:
D allows inputs and outputs to have assertions placed on them. i.e. int f(int x){ in{ assert(even(x)); } out{ assert(odd(x));; } } I would like to know if D tries to statically check these assertions. If so that would give a subtyping mechanism which would be kind of neat. If not, consider the following scenario in addition to f. int g(int x){ in{ assert(!odd(x)); } ... } Suppose I made a call: g(f(x)); Can this be made to fail by composing the assertions? Are there any tools or support for model checking and/or software verification in D outside of the core language (like Frama-C) that would support such analyses?
Dec 29 2013
Jonathan:I would like to know if D tries to statically check these assertions.Currently D doesn't statically verify them. I have an enhancement request in the works for something related, but it's not powerful enough for your use case. Bye, bearophile
Dec 29 2013
, but it's not powerful enough for your use case. Bye, bearophileIs there a link available, so that I could see what is in the making?
Jan 01 2014
Jonathan:Is there a link available, so that I could see what is in the making?Yes, this is two thirds of my proposal: http://www.digitalmars.com/d/archives/digitalmars/D/enum_pre-conditions_217595.html Bye, bearophile
Jan 01 2014