Definition of a Structured Verification in Maple - Maple Programming Help

Home : Support : Online Help : Programming : Logic : Boolean : verify : verify/structured

Definition of a Structured Verification in Maple

Description

 • A structured verification is a Maple expression other than a symbol which can be interpreted as a verification. A typical example would be $\left[\mathrm{simplify},\mathrm{simplify}\right]$. This specifies that the two objects must be lists with two operands, and that each pair of operands must have the property that their difference when simplified, equals zero.
 • This help page first gives a formal grammatical description of the valid structured verifications, then notes on some of the special verifications, and lastly, examples.
 • In the formal definition below, read "::=" to mean "is defined to be", "|" to mean "or", and "*" to mean "zero or more occurrences of".

 Syntax Matches verification ::= { verification* } alternation; any of the verifications | [ verification* ] a list of the given verifications | complex(numeric) match complex numerical constants exactly | string match strings exactly | verification = verification an equation of the corresponding verifications | verification <> verification an inequality compared with given verifications | verification < verification a relation compared with given verifications | verification <= verification a relation compared with given verifications | verification > verification a relation compared with given verifications | verification >= verification a relation compared with given verifications | verification .. verification a range compared with given verifications | verification and verification an AND of the corresponding verifications | verification or verification an OR of the corresponding verifications | not verification a NOT of the corresponding verification | verification &+ verification ... a sum of the corresponding verifications | verification &* verification ... a product of the corresponding verifications | verification &. verification ... a dot product of the corresponding verifications | verification ^ verification a power compared with the given verifications | fcnverification a function or special verification fcnverification ::= set(verification) sets of elements compared with the given verification | list(verification) lists of elements compared with the given verification | &+(verification) a sum of terms of the given verifications | &*(verification) a product of factors of the given verifications | specfunc(verification,foo) the function foo with arguments compared with the given verification | anyfunc(verification*) any functions with arguments compared with the given verifications | function(verification) any function with arguments compared with given verification | name(verification) any name with a value of the given verification | foo(verification*) a verification defined by a procedure addverify(foo::name, bar::procedure) | foo(verification*) the function foo with arguments compared with the given verifications

 • The square brackets [ and ] are used to check for a fixed argument sequence.  The verification $\left[\mathrm{boolean},\mathrm{simplify}\right]$ checks the equality of two lists, each with exactly 2 arguments, the first checked with simple equality and the second with simplify.
 • The set brackets { and } are used for alternation.  The verification {set(float(10)),list(float(10))} matches either lists or sets of floating-point numbers which are considered equal if they are within 10 units in the last place.
 • The verification $\mathrm{boolean}$ does a simple comparison.
 • The verifications $\mathrm{identical}\left(\mathrm{expr}\right)$ compares two objects, complex(numeric) or string, to the expression expr.
 • The verification $\mathrm{anyfunc}\left(\mathrm{t1},...,\mathrm{tn}\right)$ matches any two functions with $n$ arguments where the arguments agree according to the appropriate verifications.
 • The verification specfunc(ver, n) matches functions $n$ with 0 or more arguments where the arguments agree according to the verification ver.  Thus verify(f, g, specfunc(ver, n)) is equivalent to all five of the forms, type(f, function), type(g, function), $\mathrm{op}\left(0,f\right)=n$, $\mathrm{op}\left(0,g\right)=n$, and verify([op(f)], [op(g)], list(ver)).

Examples

 > $\mathrm{verify}\left(\mathrm{string},\mathrm{string},\mathrm{identical}\left(\mathrm{string}\right)\right)$
 ${\mathrm{true}}$ (1)
 > $\mathrm{verify}\left(\mathrm{evalf}\left(\mathrm{abs}\left(1,x+\mathrm{sqrt}\left(1-{\mathrm{cos}\left(2\right)}^{2}\right)\right)\right),\mathrm{abs}\left(1,x+\mathrm{sin}\left(2.\right)\right),'\mathrm{abs}\left(1,\mathrm{polynom}\left(\mathrm{float}\left(1\right),x\right)\right)'\right)$
 ${\mathrm{true}}$ (2)
 > $\mathrm{verify}\left({\left({x}^{2}-1\right)}^{2.0002},{\left(\left(x-1\right)\left(x+1\right)\right)}^{2.00003},'{\mathrm{normal}}^{\mathrm{float}\left(1.{10}^{6}\right)}'\right)$
 ${\mathrm{true}}$ (3)
 > $\mathrm{evalb}\left(\left[2.,1-{x}^{2}\right]=\left[2,\left(1-x\right)\left(1+x\right)\right]\right)$
 ${\mathrm{false}}$ (4)
 > $\mathrm{verify}\left(\left[2.0000001,1-{x}^{2}\right],\left[2,\left(1-x\right)\left(1+x\right)\right],'\left[\mathrm{float}\left(10000.\right),\mathrm{expand}\right]'\right)$
 ${\mathrm{true}}$ (5)
 > $\mathrm{verify}\left(\left\{0.32\right\},\left\{0.319996,0.320002\right\},'\mathrm{set}\left(\mathrm{float}\left(100000.\right)\right)'\right)$
 ${\mathrm{true}}$ (6)
 > $\mathrm{verify}\left(\mathrm{evalr}\left(\mathrm{sin}\left(\mathrm{INTERVAL}\left(-1..-1.5\right)\right)\right),\mathrm{INTERVAL}\left(-0.9974949866..-\mathrm{sin}\left(1\right)\right),'\mathrm{INTERVAL}\left(\mathrm{float}\left(1\right)..\mathrm{boolean}\right)'\right)$
 ${\mathrm{true}}$ (7)
 > $\mathrm{solns}≔\mathrm{dsolve}\left(\mathrm{D}\left(f\right)\left(x\right)=f\left(x\right),\left\{f\left(x\right)\right\}\right)$
 ${\mathrm{solns}}{≔}{f}{}\left({x}\right){=}{\mathrm{_C1}}{}{{ⅇ}}^{{x}}$ (8)
 > $\mathrm{verify}\left(\mathrm{solns},f\left(x\right)=\mathrm{_C1}\left(\mathrm{cosh}\left(x\right)+\mathrm{sinh}\left(x\right)\right),\mathrm{boolean}=\mathrm{testeq}\right)$
 ${\mathrm{true}}$ (9)
 > $\mathrm{zero}≔\left\{0.,c-{a}^{\mathrm{log}\left[a\right]\left(c\right)},{\mathrm{cos}\left(x\right)}^{2}+{\mathrm{sin}\left(x\right)}^{2}-1,{x}^{2}-1-\left(x-1\right)\left(x+1\right)\right\}$
 ${\mathrm{zero}}{≔}\left\{{0.}{,}{c}{-}{{a}}^{\frac{{\mathrm{ln}}{}\left({c}\right)}{{\mathrm{ln}}{}\left({a}\right)}}{,}{{x}}^{{2}}{-}{1}{-}\left({x}{-}{1}\right){}\left({x}{+}{1}\right){,}{{\mathrm{cos}}{}\left({x}\right)}^{{2}}{+}{{\mathrm{sin}}{}\left({x}\right)}^{{2}}{-}{1}\right\}$ (10)
 > $\mathrm{verify}\left(\left\{0\right\},\mathrm{zero},\mathrm{set}\left(\mathrm{simplify}\right)\right)$
 ${\mathrm{true}}$ (11)