Verify, TestYacas, LogicVerify , KnownFailure , RoundTo , VerifyArithmetic, VerifyDiv .

The Yacas test suite

This chapter describes commands used for verifying correct performance of Yacas.

Verify, TestYacas, LogicVerify verifying equivalence of two expressions
KnownFailure Mark a test as a known failure
RoundTo Round a real-valued result to a set number of digits
VerifyArithmetic, VerifyDiv Special purpose arithmetic verifiers

Yacas comes with a test suite which can be found in the directory tests/. Typing
make test
on the command line after Yacas was built will run the test. This test can be run even before make install, as it only uses files in the local directory of the Yacas source tree. The default extension for test scripts is .yts (Yacas test script).

The verification commands described in this chapter only display the expressions that do not evaluate correctly. Errors do not terminate the execution of the Yacas script that uses these testing commands, since they are meant to be used in test scripts.


Verify, TestYacas, LogicVerify -- verifying equivalence of two expressions

Standard library
Calling format:
Verify(question,answer)
TestYacas(question,answer)
LogicVerify(question,answer)

Parameters:
question -- expression to check for

answer -- expected result after evaluation

Description:
The commands Verify, TestYacas, LogicVerify can be used to verify that an expression is equivalent to a correct answer after evaluation. All three commands return True or False.

For some calculations, the demand that two expressions are identical syntactically is too stringent. The Yacas system might change at various places in the future, but 1+x would still be equivalent, from a mathematical point of view, to x+1.

The general problem of deciding that two expressions a and b are equivalent, which is the same as saying that a-b=0 , is generally hard to decide on. The following commands solve this problem by having domain-specific comparisons.

The comparison commands do the following comparison types:

Examples:
In> Verify(1+2,3)
Out> True;
In> Verify(x*(1+x),x^2+x)
******************
x*(x+1) evaluates to x*(x+1) which differs
  from x^2+x
******************
Out> False;
In> TestYacas(x*(1+x),x^2+x)
Out> True;
In> Verify(a And c Or b And Not c,a Or b)
******************
 a And c Or b And Not c evaluates to  a And c
  Or b And Not c which differs from  a Or b
******************
Out> False;
In> LogicVerify(a And c Or b And Not c,a Or b)
Out> True;
In> LogicVerify(a And c Or b And Not c,b Or a)
Out> True;

See also:
Simplify , CanProve , KnownFailure .


KnownFailure -- Mark a test as a known failure

Standard library
Calling format:
KnownFailure(test)

Parameters:
test -- expression that should return False on failure

Description:
The command KnownFailure marks a test as known to fail by displaying a message to that effect on screen.

This might be used by developers when they have no time to fix the defect, but do not wish to alarm users who download Yacas and type make test.

Examples:
In> KnownFailure(Verify(1,2))
Known failure:
******************
 1 evaluates to  1 which differs from  2
******************
Out> False;
In> KnownFailure(Verify(1,1))
Known failure:
Failure resolved!
Out> True;

See also:
Verify , TestYacas , LogicVerify .


RoundTo -- Round a real-valued result to a set number of digits

Standard library
Calling format:
RoundTo(number,precision)

Parameters:
number -- number to round off

precision -- precision to use for round-off

Description:
The function RoundTo rounds a floating point number to a specified precision, allowing for testing for correctness using the Verify command.

Examples:
In> N(RoundTo(Exp(1),30),30)
Out> 2.71828182110230114951959786552;
In> N(RoundTo(Exp(1),20),20)
Out> 2.71828182796964237096;

See also:
Verify , VerifyArithmetic , VerifyDiv .


VerifyArithmetic, VerifyDiv -- Special purpose arithmetic verifiers

Standard library
Calling format:
VerifyArithmetic(x,n,m)
RandVerifyArithmetic(n)
VerifyDiv(u,v)

Parameters:
x, n, m, u, v -- integer arguments

Description:
The commands VerifyArithmetic and VerifyDiv test a mathematic equality which should hold, testing that the result returned by the system is mathematically correct according to a mathematically provable theorem.

VerifyArithmetic verifies for an arbitrary set of numbers x, n and m that

(x^n-1)*(x^m-1)=x^(n+m)-x^n-x^m+1.

The left and right side represent two ways to arrive at the same result, and so an arithmetic module actually doing the calculation does the calculation in two different ways. The results should be exactly equal.

RandVerifyArithmetic(n) calls VerifyArithmetic with random values, n times.

VerifyDiv(u,v) checks that

u=v*Div(u,v)+Mod(u,v).

Examples:
In> VerifyArithmetic(100,50,60)
Out> True;
In> RandVerifyArithmetic(4)
Out> True;
In> VerifyDiv(x^2+2*x+3,x+1)
Out> True;
In> VerifyDiv(3,2)
Out> True;

See also:
Verify .