Dino.Verification

Documentation

verifyAssertEqStructurally :: CollectAssertions Reified a -> [(Text, Maybe (Edit NumRep))]

Check each assertEq assertion by structurally comparing the ASTs of the two expressions

This limited form of formal verification is useful two ways:

• It can be used to verify refactorings that don't affect the AST; for example, introducing a meta-level helper function (i.e. a normal Haskell function).
• When the ASTs do differ, the resulting Edit will show only the parts of the expressions where the difference occurs, which can make it easier to manually verify equivalence.

presentStructuralVerificationAsDocs :: [(Text, Maybe (Edit NumRep))] -> [Doc]

Present the output of verifyAssertEqStructurally as a list of test cases that either succeed or fail with a diff

presentStructuralVerification :: [(Text, Maybe (Edit NumRep))] -> IO ()