Implementing Rule Tests

Implementing a New Rule Test

This page aims to be a straightforward guide for developers in creating a new rule test for Aris. Testing rules is critical to ensure they behave as expected within Aris. In this example, we will create tests for ∧ Introduction, a fundamental prepositional inference rule used in logic.

Table of Contents

• Step 1: Locate the Test File
• Step 2: Create a Test Function
• Step 3: Add the Test to the Test Suite
• Step 4: Run and Verify the Test
• Step 5: Add Documentation

Step 1: Locate the Test File

Navigate to the aris/src/proofs/proof_tests.rs file. This is where proof-related unit tests are defined.

Step 2: Create a Test Function

Add a public function in the file for testing your new rule. For example, to test ∧ Introduction, create a function named test_andintro:

pub fn test_andintro<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
    use self::coproduct_inject as i; // Helper for injecting premise references
    use crate::parser::parse_unwrap as p; // Helper for parsing expressions

    let mut prf = P::new(); // Initialize a new proof

    // Step 1: Add premises to the proof
    let r1 = prf.add_premise(p("A")); // Premise A
    let r2 = prf.add_premise(p("B")); // Premise B
    let r3 = prf.add_premise(p("C")); // Premise C

    // Step 2: Test valid applications of ∧ Introduction
    let r4 = prf.add_step(Justification(
        p("A & B"),                     // Conclusion
        RuleM::AndIntro,                // Rule being tested
        vec![i(r1.clone()), i(r2.clone())], // Dependencies (A and B)
        vec![],                         // Subdependencies (none for ∧ Introduction)
    ));

    // Step 3: Test invalid applications of ∧ Introduction
    let r5 = prf.add_step(Justification(
        p("A & B"),                     // Conclusion (incorrect: C included)
        RuleM::AndIntro,
        vec![i(r1.clone()), i(r2), i(r3)], // Extra dependency (C)
        vec![],
    ));

    let r6 = prf.add_step(Justification(
        p("A & B"),                     // Conclusion (missing dependency)
        RuleM::AndIntro,
        vec![i(r1.clone())],            // Only one dependency (A)
        vec![],
    ));

    // Step 4: Test edge case applications
    let r7 = prf.add_step(Justification(
        p("A & A"),                     // Conclusion (duplicate conjuncts)
        RuleM::AndIntro,
        vec![i(r1)],                    // Dependency (A used twice)
        vec![],
    ));

    // Return the proof and categorized results for valid and invalid tests
    (prf, vec![i(r4), i(r7)], vec![i(r5), i(r6)])
}

1. Initialization:
   • A new proof instance (prf) is created using P::new().
   • Premises (r1, r2, r3) are added to the proof using prf.add_premise(...).
2. Valid Test Cases:
   • A valid application of ∧ Introduction is added using prf.add_step(...).
   • The Justification struct specifies the conclusion, rule being tested, dependencies, and subdependencies.
3. Invalid Test Cases:
   • Cases with extra dependencies (r5), missing dependencies (r6), or invalid structure are added to ensure the rule's correctness is rigorously tested.
4. Edge Cases:
   • An edge case like duplicate conjuncts (r7) is added to verify the rule handles unusual scenarios appropriately.
5. Return Values:
   • The function returns:
     • The proof instance (prf).
     • A list of valid test cases (vec![i(r4), i(r7)]).
     • A list of invalid test cases (vec![i(r5), i(r6)]).

Step 3: Add the Test to the Test Suite

Once you've written your test function (e.g., test_andintro), it must be integrated into the appropriate macro to be executed during the test suite run.

Step 3.1: Determine the Macro for Your Test

• Use the enumerate_subproofless_tests! macro if your rule does not involve subproofs.
  • For example, ∧ Introduction fits here because it only requires a list of premises and a conclusion.
• Use the enumerate_subproofful_tests! macro if your rule involves subproofs.
  • For example, rules like test_impintro (Implication Introduction) or test_notintro (Negation Introduction) require subproof handling.

Step 3.2: Add Your Test Function

1. Locate the appropriate macro (enumerate_subproofless_tests! or enumerate_subproofful_tests!) at the top of the proof_tests.rs file.
2. Add your test function name to the list within the macro. For ∧ Introduction, it goes into the enumerate_subproofless_tests! macro:

macro_rules! enumerate_subproofless_tests {
    ($x:ty, $y:ident) => {
        generate_tests! { $x, $y;
            test_andelim, test_contelim, test_orintro, test_reiteration,
            test_andintro, // Add your test here
            test_contradictionintro, test_notelim, test_impelim,
            // Other tests...
        }
    };
}

Step 4: Run and Verify the Test

To execute the test suite and verify that your rule behaves as expected:

1. Use the cargo test command to run all the tests:

cargo test

2. The generate_tests! macro will dynamically create tests for the rule using the framework's setup and will validate:
   • Whether the rule works correctly with valid premises and conclusions.
   • Whether it appropriately fails when given invalid premises, conclusions, or dependencies.
3. Review the output for your test:
   • If your test passes, it will be marked as ok.
   • If it fails, the output will include detailed information about the failure (e.g., mismatched expectations or incorrect rule behavior).

Step 5: Add Documentation

Once you have implemented your new rule test, you must add documentation into the Test Suite Documentation page. This is to ensure consistency, clarity, and traceability for Aris rule tests.

Congratulations, you've added a new rule test to Aris!