test package:sbv

Solve the equation:

2x + y - z = 2

We have:

>>> test
(k, 2+k', 2k+k')
(1+k, k', 2k+k')

That is, for arbitrary k and k', we have two different solutions. (An infinite family.) You can verify these solutuions by substituting the values for x, y and z in the above, for each choice. It's harder to see that they cover all possibilities, but a moments thought reveals that is indeed the case.

Proves the equivalence NOT (p OR (q AND r)) == (NOT p AND NOT q) OR (NOT p AND NOT r), following from the axioms we have specified above. We have:

>>> test
Q.E.D.

From Appendix A of the spec. We have:

>>> testVectors
True

Check whether an arbitrary call to checkedDiv is safe. Clearly, we do not expect this to be safe:

>>> test1
[./Documentation/SBV/Examples/Misc/NoDiv0.hs:38:14:checkedDiv: Divisor should not be 0: Violated. Model:
s0 = 0 :: Int32
s1 = 0 :: Int32]

Repeat the test, except this time we explicitly protect against the bad case. We have:

>>> test2
[./Documentation/SBV/Examples/Misc/NoDiv0.hs:46:41:checkedDiv: Divisor should not be 0: No violations detected]

Queries

Test output style

Type of test vectors (abstract)

Replacement for testBit, returning SBool instead of Bool.

Test the value of a bit. Note that we do an extract here as opposed to masking and checking against zero, as we found extraction to be much faster with large bit-vectors.

Test generation from symbolic programs

Generate a set of concrete test values from a symbolic program. The output can be rendered as test vectors in different languages as necessary. Use the function output call to indicate what fields should be in the test result. (Also see constrain for filtering acceptable test values.)

Retrieve the test vectors for further processing. This function is useful in cases where renderTest is not sufficient and custom output (or further preprocessing) is needed.

Render the test as a Haskell value with the given name n.

Writing a value, similar to how reads are done. The important thing is that the tree representation keeps updates to a minimum.

Various tests for round-trip properties. We have:

>>> runAESTests False
GOOD: Key generation AES128
GOOD: Key generation AES192
GOOD: Key generation AES256
GOOD: Encryption     AES128
GOOD: Decryption     AES128
GOOD: Decryption-OTF AES128
GOOD: Encryption     AES192
GOOD: Decryption     AES192
GOOD: Decryption-OTF AES192
GOOD: Encryption     AES256
GOOD: Decryption     AES256
GOOD: Decryption-OTF AES256

Collection of known answer tests for SHA. Since these tests take too long during regular regression runs, we pass as an argument how many to run. Increase the below number to 24 to run all tests. We have:

>>> knownAnswerTests 1
True