December 17, 2012 Value ranges from contracts? | ||||
---|---|---|---|---|
| ||||
(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 |
Copyright © 1999-2021 by the D Language Foundation