www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.learn - Do assertions provide a mechanism for subtyping? If not are they

reply "Jonathan" <jdgall84 gmail.com> writes:
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
parent reply "bearophile" <bearophileHUGS lycos.com> writes:
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
parent reply "Jonathan" <jdgall84 gmail.com> writes:
, but
 it's not powerful enough for your use case.

 Bye,
 bearophile


Is there a link available, so that I could see what is in the 
making?
Jan 01 2014
parent "bearophile" <bearophileHUGS lycos.com> writes:
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