0

This might be more suitable for Stack Overflow, but since I'm asking about the mathematical theory, rather than the implementation details, I'm initially posting the question here.

Background

The .NET 7 Framework is about to introduce an INumber<T> interface, which is designed to allow for the generic implementation of mathematical algorithms that will work with any type of number: int, float, double, decimal, etc.

However, when creating an implementation of this interface, one is only required to satisfy the signature of the interface, there is nothing inherent in the framework to ensure your interface makes sense. For instance, the INumber<T>.AdditiveIdentity is required to return an object of type T, but there's nothing inherent in the framework that would stop me setting additive identity of my type to something nonsensical.

So, I'm attempting to write a test framework that assess these implementations.

Actual Question

So, I'm starting by writing a suite of tests for the integer type, just to get into the swing of things, I'll make it generic later. The problem is, I've realised that I can only really define the common operators +-*/ in terms of eachother.

For instance, I can test that x + x = 2 * x but what is addition in the first place and how can I assess whether it's been done sensibly, even if I restrict this to the most simple case of integers.

I suppose I could test for commutivity, associativity, and that addition of the additive identity doesn't change the value (amongst some other things) and that would be a good smell test, but I'm wondering if there's anything more formal I can look for.

ScottishTapWater
  • 117
  • 1
    I'm not sure there is much more that you can test for, but one thing you could test is that adding $-a$ to $a$ gets you back to $0$. – Suzu Hirose Sep 02 '22 at 23:56
  • Good point, thanks @SuzuHirose – ScottishTapWater Sep 03 '22 at 00:01
  • What is it that you want to test? The interface of the types, or how they work? The latter you can only sample some cases, but even if you were to verify every single possible function for every single value, that doesn't prove anything. This is because functions are not mathematical functions. You can compute INumber<T>(2)+INumber<T>(2) and give you INumber<T>(4), but that doesn't imply that next time you evaluate the same expression you get the same result. – plop Sep 03 '22 at 00:19
  • @user85667 - How they work... Essentially just getting a prima facie idea of if looks like a sensible implementation. I'm planning on testing a large random sample of each type... I know I can never truly prove it. I think I can make some assumptions such as the purity and deterministic nature of the function calls. If you violate those, there's no hope! – ScottishTapWater Sep 03 '22 at 00:23
  • Are you already familiar with the Peano axioms? That's how I've seen addition formalized in languages like Haskell. – Mark S. Sep 03 '22 at 00:30
  • Up to the usual roundoff/cutoff errors, as long as the field axioms have been encoded properly by the developers, you shouldn’t have an issue. Of course you can always input nonsensical information, but that is up to the user to put in correct data to the signature. Also, in light of errors, choosing a threshold for what you consider zero is a good way to go. – Kevin Sep 03 '22 at 00:57

1 Answers1

1

This is an interesting problem, and one that computer scientists have thought about quite a bit.

The problem with testing is that tests can, in most cases, only reveal the presence of bugs. They cannot prove the absence of bugs. So the problem of testing a property is rather complex.

An alternative is attempting to prove that the program is correct. The issue is that a program can be correct even if there is no proof that it is correct. And there is certainly no algorithm to determine whether a program meets a specification. Even if you could prove your program correct, you would then have to worry about whether your proof is correct (though you could do the proof in an automated proof checker to lessen this risk).

Finally, if you look at how a C# compiler actually implements integer addition, you’ll see that it delegates the operation to your CPU. So you moreover have to blindly trust that your CPU is correct.

The practical approach is to generate a large test suite which includes plausible edge cases and random test generation (eg, randomly generated an $x$ and check whether $x + x = 2x$). You should focus on verifying that the basic axioms hold; equations like $x + x = 2x$ can be derived from more basic axioms and thus don’t really need to be tested themselves, though it can’t hurt.

This approach has its own issues if you attempt to automatically generate a test suite for an arbitrary implementation of INumber. There are an unbelievable number of mathematical “fields” which could satisfy the constraints imposed by INumber, and it is hopeless to even attempt to find a way to automatically generate test cases appropriate for each such field that could be implemented on a computer.

Mark Saving
  • 31,855