Does D have any methods of validating code in a natural manner besides unit tests and contracts?

I'm specifically thinking of validating mathematical calculations and boolean operations that could depend on very improbable scenarios but are technically invalid logic.

These issues tend to creep up in calculations that involve floating points due to various reasons or comparisons that mistakenly use > for >= or vice versa.

If I have a variable such as a buffer which has a length and an offset in to that buffer is calculated using double precision then rounding errors could cause the offset to except the length and create an access violation.

To be able to theoretically test all the possibilities all valid inputs would need to be checked. One can setup unit tests to test these possibilities but it can be difficult to cover all cases in even a semi-complex program.

Just curious if something exists that allows for mathematical validation such code in an relatively canonical way. This isn't too hard for pure functions but dealing with non-pure functions can be a pain.

On Monday, 4 June 2018 at 15:48:35 UTC, DigitalDesigns wrote:
> Does D have any methods of validating code in a natural manner besides unit tests and contracts?
>
> I'm specifically thinking of validating mathematical calculations and boolean operations that could depend on very improbable scenarios but are technically invalid logic.
>
> These issues tend to creep up in calculations that involve floating points due to various reasons or comparisons that mistakenly use > for >= or vice versa.
>
> If I have a variable such as a buffer which has a length and an offset in to that buffer is calculated using double precision then rounding errors could cause the offset to except the length and create an access violation.
>
> To be able to theoretically test all the possibilities all valid inputs would need to be checked. One can setup unit tests to test these possibilities but it can be difficult to cover all cases in even a semi-complex program.
>
> Just curious if something exists that allows for mathematical validation such code in an relatively canonical way. This isn't too hard for pure functions but dealing with non-pure functions can be a pain.

Perhaps not quite what you're looking for, but I think you would be interested in the LLVM fuzzing part of Johan Engelen's talk at DConf 2018:
https://www.youtube.com/watch?v=GMKvYrjaaoU (at around 34:30).

On Monday, 4 June 2018 at 15:48:35 UTC, DigitalDesigns wrote:
> Just curious if something exists that allows for mathematical validation such code in an relatively canonical way. This isn't too hard for pure functions but dealing with non-pure functions can be a pain.

Something like HACL? https://github.com/mitls/hacl-c

On Tuesday, 5 June 2018 at 06:45:31 UTC, Petar Kirov [ZombineDev] wrote:
> On Monday, 4 June 2018 at 15:48:35 UTC, DigitalDesigns wrote:
>> Does D have any methods of validating code in a natural manner besides unit tests and contracts?
>>
>> I'm specifically thinking of validating mathematical calculations and boolean operations that could depend on very improbable scenarios but are technically invalid logic.
>>
>> These issues tend to creep up in calculations that involve floating points due to various reasons or comparisons that mistakenly use > for >= or vice versa.
>>
>> If I have a variable such as a buffer which has a length and an offset in to that buffer is calculated using double precision then rounding errors could cause the offset to except the length and create an access violation.
>>
>> To be able to theoretically test all the possibilities all valid inputs would need to be checked. One can setup unit tests to test these possibilities but it can be difficult to cover all cases in even a semi-complex program.
>>
>> Just curious if something exists that allows for mathematical validation such code in an relatively canonical way. This isn't too hard for pure functions but dealing with non-pure functions can be a pain.
>
> Perhaps not quite what you're looking for, but I think you would be interested in the LLVM fuzzing part of Johan Engelen's talk at DConf 2018:
> https://www.youtube.com/watch?v=GMKvYrjaaoU (at around 34:30).

Sorta, but not fuzzing because that is too spare. Rather than picking a random point in a billion dimensional vector space bit is sort of works only on the surface of possible values. Which he addresses initially being the problem and is similar to what I'm looking for.

The idea though is problems almost always occur on edge cases so there is no need to check everything inside an interval but only the edge cases.

if (x < 10)

one only needs to check if x = 9, 10, 11 but not 4, 5, etc.

Of course, in more complex cases it might be difficult to determine this so maybe the method in the video is more general purpose. It seems to have the capabilities to have a bit more intelligent checking though so yeah, this seems to be what I was looking for!

Thanks!



In any case