This class indicates that the error type to can always represent the error type from.

This is useful in implementing generic procedures that may throw errors. For example, we support symbolic division and modulo operations. These operations should throw an error when the divisor is zero, and we use the standard error type ArithException for this purpose. However, the user may use other type to represent errors, so we need this type class to transform the ArithException to the user-defined types.

Another example of these generic procedures is the symAssert and symAssume functions. They can be used with any error types that are compatible with the AssertionError and VerificationConditions types, respectively.

Used within a monadic multi path computation for exception processing.

Terminate the current execution path with the specified error if the condition does not hold. Compatible error can be transformed.

>>> let assert = symAssertTransformableError AssertionError
>>> assert "a" :: ExceptT AssertionError UnionM ()
ExceptT {If (! a) (Left AssertionError) (Right ())}

Used within a monadic multi path computation to begin exception processing.

Terminate the current execution path with the specified error. Compatible errors can be transformed.

>>> symThrowTransformableError Overflow :: ExceptT AssertionError UnionM ()
ExceptT {Left AssertionError}

Used within a monadic multi path computation to begin exception processing.

Checks the condition passed to the function. The current execution path will be terminated with assertion error if the condition is false.

If the condition is symbolic, Grisette will split the execution into two paths based on the condition. The symbolic execution will continue on the then-branch, where the condition is true. For the else branch, where the condition is false, the execution will be terminated.

The resulting monadic environment should be compatible with the AssertionError error type. See TransformError type class for details.

Examples:

Terminates the execution if the condition is false. Note that we may lose the Mergeable knowledge here if no possible execution path is viable. This may affect the efficiency in theory, but in practice this should not be a problem as all paths are terminated and no further evaluation would be performed.

>>> symAssert (con False) :: ExceptT AssertionError UnionM ()
ExceptT {Left AssertionError}
>>> do; symAssert (con False); mrgReturn 1 :: ExceptT AssertionError UnionM Integer
ExceptT <Left AssertionError>

No effect if the condition is true:

>>> symAssert (con True) :: ExceptT AssertionError UnionM ()
ExceptT {Right ()}
>>> do; symAssert (con True); mrgReturn 1 :: ExceptT AssertionError UnionM Integer
ExceptT {Right 1}

Splitting the path and terminate one of them when the condition is symbolic.

>>> symAssert (ssym "a") :: ExceptT AssertionError UnionM ()
ExceptT {If (! a) (Left AssertionError) (Right ())}
>>> do; symAssert (ssym "a"); mrgReturn 1 :: ExceptT AssertionError UnionM Integer
ExceptT {If (! a) (Left AssertionError) (Right 1)}

AssertionError is compatible with VerificationConditions:

>>> symAssert (ssym "a") :: ExceptT VerificationConditions UnionM ()
ExceptT {If (! a) (Left AssertionViolation) (Right ())}

Used within a monadic multi path computation to begin exception processing.

Similar to symAssert, but terminates the execution path with AssumptionViolation error.

Examples:

>>> symAssume (ssym "a") :: ExceptT VerificationConditions UnionM ()
ExceptT {If (! a) (Left AssumptionViolation) (Right ())}