Value ranges from contracts?
bearophile
bearophileHUGS at lycos.com
Mon Dec 17 15:29:33 PST 2012
(This comes after the recent "Troubles with user defined
subtypes" post of mine).
Is it a good idea to improve the D value range analysis to
support code like this?
void foo(immutable int x) pure nothrow
in {
assert(x >= '0' && x <= '9');
} body {
char c = x; // error, cast required.
}
void main() {}
Currently you have to write this because, despite that
pre-condition, the D type system can't see it's a safe assignment:
char c = cast(char)x;
D ignores lot of potentially useful semantics contained in
contracts, they are quite under-used. There are languages like
Whiley that are good at those things, but note this improvement
of D value range analysis doesn't require flow analyis (unlike
Whiley because x is immutable, so once the pre-condition pass, x
is a correct digit in every code paths inside the foo body{}.
http://whiley.org/2012/12/04/generating-verification-conditions-for-whiley/
Bye,
bearophile
More information about the Digitalmars-d
mailing list