Equation Solving

One of the side benefits of the NStatic Tool is the ability to solve various types of equations or systems of equations. One set of problems is the solving of systems of equations in linear algebra.

In the example above, we have three equations with three unknowns. Since all three equations are linearly independent, we are guaranteed a single solution as revealed below by NStatic.

I kept the parameter types as doubles, since even though all the coefficients are integers, we could easily get a solution set that incorporates numbers from the rational domain.

Just by changing the integer constant in the right hand side of the last equation from 10 to 11, all of the values would have to be rationals, and last assert would no longer be satisfiable if any of the parameter variables were declared an int.

The value column depicts all of the solutions values in rational form (with a numerator and denominator), even though they were declared as doubles. The use of rational numbers ensures against rounding errors, which could easily introduce hard-to-find bugs into the system.

Another set of problems are polynomial equations. NStatic has the ability to solve polynomial equalities and inequalities. Nonlinear equations arise quite commonly with recursion and looping control structures.

Here I have a loop that computes the sum of an arithmetic sequence and then performs a test on the sum.

In this case, we are able to place a bound on the value of n to ensure that the sum is over 20. The variable sum is a quadratic polynomial of a complex term, so we can find the roots of the equation to come out with a disjunction of all the possible ranges of n.

 

Comments

[Kirill Osenkov]

This looks really impressive - I can't remember such a deep integration of symbolic algebra in a programming tool. It somewhat reminds me of Epigram ( http://www.e-pig.org ), but unlike Epigram NStatic will hopefully be an industrial strenth tool, not only a research prototype.

So does this solving algorithm also work with custom-implemented Assert methods? Say, I have

void Assert(bool condition)
{
if (!condition) throw new AssertionFailedException();
}

[Wesner Moise]

Yes, works against exceptions as well as asserts.