Skip to main content

quantrs2_anneal/advanced_testing_framework/
property_tester.rs

1//! Property-based testing system
2
3use super::{
4    ApplicationError, ApplicationResult, ConstraintSpec, DensitySpec, Duration, GenerationStrategy,
5    HashMap, Instant, InvariantScope, ProblemSpecification, ProblemType, PropertyTestResult,
6    PropertyType, PropertyValue, TestExecutionResult,
7};
8use scirs2_core::random::{thread_rng, Rng};
9
10/// Property-based testing system
11#[derive(Debug)]
12pub struct PropertyBasedTester {
13    /// Property definitions
14    pub properties: Vec<PropertyDefinition>,
15    /// Test case generators
16    pub generators: Vec<TestCaseGenerator>,
17    /// Shrinking strategies
18    pub shrinking_strategies: Vec<ShrinkingStrategy>,
19    /// Execution statistics
20    pub execution_stats: PropertyTestStats,
21}
22
23/// Property definition for testing
24#[derive(Debug)]
25pub struct PropertyDefinition {
26    /// Property identifier
27    pub id: String,
28    /// Property description
29    pub description: String,
30    /// Property type
31    pub property_type: PropertyType,
32    /// Preconditions
33    pub preconditions: Vec<Precondition>,
34    /// Postconditions
35    pub postconditions: Vec<Postcondition>,
36    /// Invariants
37    pub invariants: Vec<Invariant>,
38}
39
40/// Precondition for property
41#[derive(Debug, Clone)]
42pub struct Precondition {
43    /// Condition identifier
44    pub id: String,
45    /// Condition expression
46    pub expression: String,
47    /// Condition parameters
48    pub parameters: HashMap<String, f64>,
49}
50
51/// Postcondition for property
52#[derive(Debug, Clone)]
53pub struct Postcondition {
54    /// Condition identifier
55    pub id: String,
56    /// Condition expression
57    pub expression: String,
58    /// Expected result
59    pub expected_result: PropertyValue,
60    /// Tolerance
61    pub tolerance: f64,
62}
63
64/// Invariant for property
65#[derive(Debug, Clone)]
66pub struct Invariant {
67    /// Invariant identifier
68    pub id: String,
69    /// Invariant expression
70    pub expression: String,
71    /// Invariant scope
72    pub scope: InvariantScope,
73}
74
75/// Test case generator for property-based testing
76#[derive(Debug)]
77pub struct TestCaseGenerator {
78    /// Generator identifier
79    pub id: String,
80    /// Generation strategy
81    pub strategy: GenerationStrategy,
82    /// Size bounds
83    pub size_bounds: (usize, usize),
84    /// Generation parameters
85    pub parameters: HashMap<String, f64>,
86}
87
88/// Shrinking strategy for failed test cases
89#[derive(Debug)]
90pub struct ShrinkingStrategy {
91    /// Strategy identifier
92    pub id: String,
93    /// Shrinking algorithm
94    pub algorithm: ShrinkingAlgorithm,
95    /// Maximum shrinking attempts
96    pub max_attempts: usize,
97    /// Shrinking parameters
98    pub parameters: HashMap<String, f64>,
99}
100
101/// Shrinking algorithms
102#[derive(Debug, Clone, PartialEq, Eq)]
103pub enum ShrinkingAlgorithm {
104    /// Linear shrinking
105    Linear,
106    /// Binary search shrinking
107    BinarySearch,
108    /// Delta debugging
109    DeltaDebugging,
110    /// Custom shrinking
111    Custom(String),
112}
113
114/// Property test execution statistics
115#[derive(Debug, Default)]
116pub struct PropertyTestStats {
117    /// Total test cases generated
118    pub cases_generated: usize,
119    /// Test cases that passed
120    pub cases_passed: usize,
121    /// Test cases that failed
122    pub cases_failed: usize,
123    /// Shrinking attempts made
124    pub shrinking_attempts: usize,
125    /// Total execution time
126    pub execution_time: Duration,
127}
128
129impl PropertyBasedTester {
130    #[must_use]
131    pub fn new() -> Self {
132        Self {
133            properties: Self::create_default_properties(),
134            generators: Self::create_default_generators(),
135            shrinking_strategies: Self::create_default_shrinking_strategies(),
136            execution_stats: PropertyTestStats::default(),
137        }
138    }
139
140    /// Create default property definitions
141    fn create_default_properties() -> Vec<PropertyDefinition> {
142        vec![
143            PropertyDefinition {
144                id: "solution_feasibility".to_string(),
145                description: "All solutions must be feasible".to_string(),
146                property_type: PropertyType::Correctness,
147                preconditions: vec![Precondition {
148                    id: "valid_problem".to_string(),
149                    expression: "problem.is_valid()".to_string(),
150                    parameters: HashMap::new(),
151                }],
152                postconditions: vec![Postcondition {
153                    id: "solution_valid".to_string(),
154                    expression: "solution.is_feasible()".to_string(),
155                    expected_result: PropertyValue::Boolean(true),
156                    tolerance: 0.0,
157                }],
158                invariants: vec![Invariant {
159                    id: "energy_conservation".to_string(),
160                    expression: "energy_is_conserved".to_string(),
161                    scope: InvariantScope::Global,
162                }],
163            },
164            PropertyDefinition {
165                id: "optimization_monotonicity".to_string(),
166                description: "Optimization should improve or maintain solution quality".to_string(),
167                property_type: PropertyType::Performance,
168                preconditions: vec![Precondition {
169                    id: "initial_solution".to_string(),
170                    expression: "has_initial_solution".to_string(),
171                    parameters: HashMap::new(),
172                }],
173                postconditions: vec![Postcondition {
174                    id: "quality_improvement".to_string(),
175                    expression: "final_quality >= initial_quality".to_string(),
176                    expected_result: PropertyValue::Boolean(true),
177                    tolerance: 0.001,
178                }],
179                invariants: vec![Invariant {
180                    id: "quality_monotonic".to_string(),
181                    expression: "quality_non_decreasing".to_string(),
182                    scope: InvariantScope::Temporal,
183                }],
184            },
185            PropertyDefinition {
186                id: "deterministic_behavior".to_string(),
187                description: "Same input should produce same output with fixed seed".to_string(),
188                property_type: PropertyType::Consistency,
189                preconditions: vec![Precondition {
190                    id: "fixed_seed".to_string(),
191                    expression: "seed.is_fixed()".to_string(),
192                    parameters: HashMap::new(),
193                }],
194                postconditions: vec![Postcondition {
195                    id: "reproducible_result".to_string(),
196                    expression: "result1 == result2".to_string(),
197                    expected_result: PropertyValue::Boolean(true),
198                    tolerance: 0.0,
199                }],
200                invariants: Vec::new(),
201            },
202            PropertyDefinition {
203                id: "resource_bounds".to_string(),
204                description: "Resource usage should remain within bounds".to_string(),
205                property_type: PropertyType::Safety,
206                preconditions: Vec::new(),
207                postconditions: vec![
208                    Postcondition {
209                        id: "memory_bounded".to_string(),
210                        expression: "memory_usage <= max_memory".to_string(),
211                        expected_result: PropertyValue::Boolean(true),
212                        tolerance: 0.0,
213                    },
214                    Postcondition {
215                        id: "time_bounded".to_string(),
216                        expression: "execution_time <= max_time".to_string(),
217                        expected_result: PropertyValue::Boolean(true),
218                        tolerance: 0.0,
219                    },
220                ],
221                invariants: vec![Invariant {
222                    id: "resource_limits".to_string(),
223                    expression: "within_resource_limits".to_string(),
224                    scope: InvariantScope::Global,
225                }],
226            },
227        ]
228    }
229
230    /// Create default test case generators
231    fn create_default_generators() -> Vec<TestCaseGenerator> {
232        vec![
233            TestCaseGenerator {
234                id: "random_ising_generator".to_string(),
235                strategy: GenerationStrategy::Random,
236                size_bounds: (5, 100),
237                parameters: {
238                    let mut params = HashMap::new();
239                    params.insert("density".to_string(), 0.3);
240                    params.insert("bias_range".to_string(), 2.0);
241                    params.insert("coupling_range".to_string(), 1.0);
242                    params
243                },
244            },
245            TestCaseGenerator {
246                id: "boundary_value_generator".to_string(),
247                strategy: GenerationStrategy::BoundaryValue,
248                size_bounds: (1, 1000),
249                parameters: {
250                    let mut params = HashMap::new();
251                    params.insert("boundary_offset".to_string(), 1.0);
252                    params
253                },
254            },
255            TestCaseGenerator {
256                id: "equivalence_class_generator".to_string(),
257                strategy: GenerationStrategy::EquivalenceClass,
258                size_bounds: (10, 50),
259                parameters: {
260                    let mut params = HashMap::new();
261                    params.insert("num_classes".to_string(), 5.0);
262                    params
263                },
264            },
265        ]
266    }
267
268    /// Create default shrinking strategies
269    fn create_default_shrinking_strategies() -> Vec<ShrinkingStrategy> {
270        vec![
271            ShrinkingStrategy {
272                id: "linear_shrinking".to_string(),
273                algorithm: ShrinkingAlgorithm::Linear,
274                max_attempts: 100,
275                parameters: {
276                    let mut params = HashMap::new();
277                    params.insert("shrink_factor".to_string(), 0.5);
278                    params
279                },
280            },
281            ShrinkingStrategy {
282                id: "binary_search_shrinking".to_string(),
283                algorithm: ShrinkingAlgorithm::BinarySearch,
284                max_attempts: 50,
285                parameters: HashMap::new(),
286            },
287            ShrinkingStrategy {
288                id: "delta_debugging".to_string(),
289                algorithm: ShrinkingAlgorithm::DeltaDebugging,
290                max_attempts: 200,
291                parameters: {
292                    let mut params = HashMap::new();
293                    params.insert("granularity".to_string(), 2.0);
294                    params
295                },
296            },
297        ]
298    }
299
300    /// Run property-based tests
301    pub fn run_property_tests(
302        &mut self,
303        property_id: &str,
304        num_cases: usize,
305    ) -> ApplicationResult<PropertyTestResult> {
306        let property = self
307            .properties
308            .iter()
309            .find(|p| p.id == property_id)
310            .ok_or_else(|| {
311                ApplicationError::ConfigurationError(format!("Property not found: {property_id}"))
312            })?
313            .clone();
314
315        println!("Running property-based tests for: {}", property.id);
316        let start_time = Instant::now();
317
318        let mut cases_tested = 0;
319        let mut cases_passed = 0;
320        let mut counterexamples = Vec::new();
321
322        // Generate and test cases
323        for _ in 0..num_cases {
324            let test_case = self.generate_test_case(&property)?;
325            cases_tested += 1;
326
327            let result = self.test_property(&property, &test_case)?;
328
329            if result.passed {
330                cases_passed += 1;
331            } else {
332                // Try to shrink the counterexample
333                let shrunk_case = {
334                    self.execution_stats.shrinking_attempts += 1;
335                    self.shrink_counterexample_internal(&property, &test_case)?
336                };
337                counterexamples.push(format!("Case {cases_tested}: {shrunk_case:?}"));
338
339                // For demonstration, stop after finding a few counterexamples
340                if counterexamples.len() >= 3 {
341                    break;
342                }
343            }
344        }
345
346        let execution_time = start_time.elapsed();
347        let confidence = if cases_tested > 0 {
348            cases_passed as f64 / cases_tested as f64
349        } else {
350            0.0
351        };
352
353        // Update statistics
354        self.execution_stats.cases_generated += cases_tested;
355        self.execution_stats.cases_passed += cases_passed;
356        self.execution_stats.cases_failed += cases_tested - cases_passed;
357        self.execution_stats.execution_time += execution_time;
358
359        println!("Property test completed: {cases_passed}/{cases_tested} passed");
360
361        Ok(PropertyTestResult {
362            property_id: property.id.clone(),
363            cases_tested,
364            cases_passed,
365            counterexamples,
366            confidence,
367            execution_time,
368        })
369    }
370
371    /// Generate test case for property
372    fn generate_test_case(
373        &self,
374        property: &PropertyDefinition,
375    ) -> ApplicationResult<PropertyTestCase> {
376        // Find appropriate generator
377        let generator = self
378            .generators
379            .iter()
380            .find(|g| self.is_generator_suitable(g, property))
381            .ok_or_else(|| {
382                ApplicationError::ConfigurationError(
383                    "No suitable generator found for property".to_string(),
384                )
385            })?;
386
387        self.generate_with_strategy(generator, property)
388    }
389
390    /// Check if generator is suitable for property
391    const fn is_generator_suitable(
392        &self,
393        _generator: &TestCaseGenerator,
394        _property: &PropertyDefinition,
395    ) -> bool {
396        // Simplified: assume all generators are suitable
397        true
398    }
399
400    /// Generate test case with specific strategy
401    fn generate_with_strategy(
402        &self,
403        generator: &TestCaseGenerator,
404        _property: &PropertyDefinition,
405    ) -> ApplicationResult<PropertyTestCase> {
406        match generator.strategy {
407            GenerationStrategy::Random => self.generate_random_case(generator),
408            GenerationStrategy::BoundaryValue => self.generate_boundary_case(generator),
409            GenerationStrategy::EquivalenceClass => self.generate_equivalence_case(generator),
410            _ => self.generate_random_case(generator), // Fallback
411        }
412    }
413
414    /// Generate random test case
415    fn generate_random_case(
416        &self,
417        generator: &TestCaseGenerator,
418    ) -> ApplicationResult<PropertyTestCase> {
419        let mut rng = thread_rng();
420        let size = rng.random_range(generator.size_bounds.0..=generator.size_bounds.1);
421
422        let density = generator.parameters.get("density").unwrap_or(&0.3);
423        let bias_range = generator.parameters.get("bias_range").unwrap_or(&1.0);
424
425        Ok(PropertyTestCase {
426            id: format!("random_case_{}", thread_rng().random::<u32>()),
427            problem_spec: ProblemSpecification {
428                problem_type: ProblemType::RandomIsing,
429                size_range: (size, size),
430                density: DensitySpec {
431                    edge_density: (*density, *density),
432                    constraint_density: None,
433                    bias_sparsity: None,
434                },
435                constraints: ConstraintSpec {
436                    num_constraints: None,
437                    constraint_types: Vec::new(),
438                    strength_range: (0.1, *bias_range),
439                },
440                seed: Some(rng.random()),
441            },
442            input_parameters: {
443                let mut params = HashMap::new();
444                params.insert("size".to_string(), PropertyValue::Numeric(size as f64));
445                params.insert("density".to_string(), PropertyValue::Numeric(*density));
446                params
447            },
448            expected_properties: Vec::new(),
449        })
450    }
451
452    /// Generate boundary value test case
453    fn generate_boundary_case(
454        &self,
455        generator: &TestCaseGenerator,
456    ) -> ApplicationResult<PropertyTestCase> {
457        // Use boundary values: minimum, maximum, and near-boundary values
458        let boundary_sizes = vec![
459            generator.size_bounds.0,
460            generator.size_bounds.0 + 1,
461            generator.size_bounds.1 - 1,
462            generator.size_bounds.1,
463        ];
464
465        let mut rng = thread_rng();
466        let size = boundary_sizes[rng.random_range(0..boundary_sizes.len())];
467
468        Ok(PropertyTestCase {
469            id: format!("boundary_case_{size}"),
470            problem_spec: ProblemSpecification {
471                problem_type: ProblemType::RandomIsing,
472                size_range: (size, size),
473                density: DensitySpec {
474                    edge_density: (0.1, 0.1),
475                    constraint_density: None,
476                    bias_sparsity: None,
477                },
478                constraints: ConstraintSpec {
479                    num_constraints: None,
480                    constraint_types: Vec::new(),
481                    strength_range: (0.1, 1.0),
482                },
483                seed: Some(42),
484            },
485            input_parameters: {
486                let mut params = HashMap::new();
487                params.insert("size".to_string(), PropertyValue::Numeric(size as f64));
488                params.insert(
489                    "boundary_type".to_string(),
490                    PropertyValue::String("size_boundary".to_string()),
491                );
492                params
493            },
494            expected_properties: Vec::new(),
495        })
496    }
497
498    /// Generate equivalence class test case
499    fn generate_equivalence_case(
500        &self,
501        generator: &TestCaseGenerator,
502    ) -> ApplicationResult<PropertyTestCase> {
503        let num_classes = *generator.parameters.get("num_classes").unwrap_or(&5.0) as usize;
504        let mut rng = thread_rng();
505        let class_id = rng.random_range(0..num_classes);
506
507        // Define equivalence classes based on problem characteristics
508        let (problem_type, density) = match class_id {
509            0 => (ProblemType::RandomIsing, 0.1), // Sparse problems
510            1 => (ProblemType::RandomIsing, 0.5), // Dense problems
511            2 => (ProblemType::MaxCut, 0.3),      // MaxCut problems
512            3 => (ProblemType::VertexCover, 0.2), // VertexCover problems
513            _ => (ProblemType::RandomIsing, 0.3), // Default class
514        };
515
516        let mut rng = thread_rng();
517        let size = rng.random_range(generator.size_bounds.0..=generator.size_bounds.1);
518
519        Ok(PropertyTestCase {
520            id: format!("equiv_case_{class_id}_{size}"),
521            problem_spec: ProblemSpecification {
522                problem_type,
523                size_range: (size, size),
524                density: DensitySpec {
525                    edge_density: (density, density),
526                    constraint_density: None,
527                    bias_sparsity: None,
528                },
529                constraints: ConstraintSpec {
530                    num_constraints: None,
531                    constraint_types: Vec::new(),
532                    strength_range: (0.1, 1.0),
533                },
534                seed: Some(42 + class_id as u64),
535            },
536            input_parameters: {
537                let mut params = HashMap::new();
538                params.insert(
539                    "equivalence_class".to_string(),
540                    PropertyValue::Numeric(class_id as f64),
541                );
542                params.insert("size".to_string(), PropertyValue::Numeric(size as f64));
543                params
544            },
545            expected_properties: Vec::new(),
546        })
547    }
548
549    /// Test property against test case
550    fn test_property(
551        &self,
552        property: &PropertyDefinition,
553        test_case: &PropertyTestCase,
554    ) -> ApplicationResult<PropertyTestCaseResult> {
555        // Check preconditions
556        for precondition in &property.preconditions {
557            if !self.evaluate_precondition(precondition, test_case)? {
558                return Ok(PropertyTestCaseResult {
559                    test_case_id: test_case.id.clone(),
560                    passed: false,
561                    failure_reason: Some(format!("Precondition failed: {}", precondition.id)),
562                    execution_time: Duration::from_millis(1),
563                    property_values: HashMap::new(),
564                });
565            }
566        }
567
568        // Execute the test (simplified simulation)
569        let start_time = Instant::now();
570        let execution_result = self.simulate_test_execution(test_case)?;
571        let execution_time = start_time.elapsed();
572
573        // Check postconditions
574        let mut all_passed = true;
575        let mut failure_reason = None;
576        let mut property_values = HashMap::new();
577
578        for postcondition in &property.postconditions {
579            let result = self.evaluate_postcondition(postcondition, &execution_result)?;
580            property_values.insert(postcondition.id.clone(), result.actual_value.clone());
581
582            if !result.passed {
583                all_passed = false;
584                failure_reason = Some(format!(
585                    "Postcondition failed: {} (expected: {:?}, actual: {:?})",
586                    postcondition.id, postcondition.expected_result, result.actual_value
587                ));
588                break;
589            }
590        }
591
592        // Check invariants
593        if all_passed {
594            for invariant in &property.invariants {
595                if !self.evaluate_invariant(invariant, &execution_result)? {
596                    all_passed = false;
597                    failure_reason = Some(format!("Invariant violated: {}", invariant.id));
598                    break;
599                }
600            }
601        }
602
603        Ok(PropertyTestCaseResult {
604            test_case_id: test_case.id.clone(),
605            passed: all_passed,
606            failure_reason,
607            execution_time,
608            property_values,
609        })
610    }
611
612    /// Evaluate precondition
613    const fn evaluate_precondition(
614        &self,
615        _precondition: &Precondition,
616        _test_case: &PropertyTestCase,
617    ) -> ApplicationResult<bool> {
618        // Simplified: assume all preconditions pass
619        Ok(true)
620    }
621
622    /// Simulate test execution
623    fn simulate_test_execution(
624        &self,
625        test_case: &PropertyTestCase,
626    ) -> ApplicationResult<TestExecutionResult> {
627        let size = match test_case.input_parameters.get("size") {
628            Some(PropertyValue::Numeric(s)) => *s as usize,
629            _ => 10,
630        };
631
632        // Simulate execution with some variability
633        let quality = thread_rng().random::<f64>().mul_add(0.2, 0.8);
634        let execution_time = Duration::from_millis((size as u64 * 10).min(1000));
635
636        Ok(TestExecutionResult {
637            solution_quality: quality,
638            execution_time,
639            final_energy: -quality * size as f64,
640            best_solution: vec![1; size],
641            convergence_achieved: quality > 0.9,
642            memory_used: size * 8,
643        })
644    }
645
646    /// Evaluate postcondition
647    fn evaluate_postcondition(
648        &self,
649        postcondition: &Postcondition,
650        execution_result: &TestExecutionResult,
651    ) -> ApplicationResult<PostconditionResult> {
652        let actual_value = match postcondition.id.as_str() {
653            "solution_valid" => PropertyValue::Boolean(execution_result.convergence_achieved),
654            "quality_improvement" => PropertyValue::Numeric(execution_result.solution_quality),
655            "reproducible_result" => PropertyValue::Boolean(true), // Simplified
656            "memory_bounded" => PropertyValue::Boolean(execution_result.memory_used < 1_000_000),
657            "time_bounded" => {
658                PropertyValue::Boolean(execution_result.execution_time < Duration::from_secs(60))
659            }
660            _ => PropertyValue::Boolean(true),
661        };
662
663        let passed = match (&postcondition.expected_result, &actual_value) {
664            (PropertyValue::Boolean(expected), PropertyValue::Boolean(actual)) => {
665                expected == actual
666            }
667            (PropertyValue::Numeric(expected), PropertyValue::Numeric(actual)) => {
668                (expected - actual).abs() <= postcondition.tolerance
669            }
670            _ => false,
671        };
672
673        Ok(PostconditionResult {
674            postcondition_id: postcondition.id.clone(),
675            passed,
676            expected_value: postcondition.expected_result.clone(),
677            actual_value,
678            deviation: 0.0, // Simplified
679        })
680    }
681
682    /// Evaluate invariant
683    const fn evaluate_invariant(
684        &self,
685        _invariant: &Invariant,
686        _execution_result: &TestExecutionResult,
687    ) -> ApplicationResult<bool> {
688        // Simplified: assume all invariants hold
689        Ok(true)
690    }
691
692    /// Shrink counterexample to minimal failing case (internal, doesn't update stats)
693    fn shrink_counterexample_internal(
694        &self,
695        _property: &PropertyDefinition,
696        test_case: &PropertyTestCase,
697    ) -> ApplicationResult<PropertyTestCase> {
698        // Simplified shrinking: just reduce problem size
699        let current_size = match test_case.input_parameters.get("size") {
700            Some(PropertyValue::Numeric(s)) => (*s as usize).max(1),
701            _ => 1,
702        };
703
704        let shrunk_size = (current_size / 2).max(1);
705
706        let mut shrunk_case = test_case.clone();
707        shrunk_case.id = format!("{}_shrunk", test_case.id);
708        shrunk_case.problem_spec.size_range = (shrunk_size, shrunk_size);
709        shrunk_case.input_parameters.insert(
710            "size".to_string(),
711            PropertyValue::Numeric(shrunk_size as f64),
712        );
713
714        Ok(shrunk_case)
715    }
716
717    /// Add property definition
718    pub fn add_property(&mut self, property: PropertyDefinition) {
719        self.properties.push(property);
720    }
721
722    /// Get property by ID
723    #[must_use]
724    pub fn get_property(&self, property_id: &str) -> Option<&PropertyDefinition> {
725        self.properties.iter().find(|p| p.id == property_id)
726    }
727
728    /// Add test case generator
729    pub fn add_generator(&mut self, generator: TestCaseGenerator) {
730        self.generators.push(generator);
731    }
732
733    /// Get execution statistics
734    #[must_use]
735    pub const fn get_stats(&self) -> &PropertyTestStats {
736        &self.execution_stats
737    }
738}
739
740/// Test case for property-based testing
741#[derive(Debug, Clone)]
742pub struct PropertyTestCase {
743    /// Test case identifier
744    pub id: String,
745    /// Problem specification
746    pub problem_spec: ProblemSpecification,
747    /// Input parameters
748    pub input_parameters: HashMap<String, PropertyValue>,
749    /// Expected properties to hold
750    pub expected_properties: Vec<String>,
751}
752
753/// Result from property test case execution
754#[derive(Debug)]
755pub struct PropertyTestCaseResult {
756    /// Test case identifier
757    pub test_case_id: String,
758    /// Whether the test passed
759    pub passed: bool,
760    /// Failure reason (if failed)
761    pub failure_reason: Option<String>,
762    /// Execution time
763    pub execution_time: Duration,
764    /// Property values observed
765    pub property_values: HashMap<String, PropertyValue>,
766}
767
768/// Result from postcondition evaluation
769#[derive(Debug)]
770pub struct PostconditionResult {
771    /// Postcondition identifier
772    pub postcondition_id: String,
773    /// Whether postcondition passed
774    pub passed: bool,
775    /// Expected value
776    pub expected_value: PropertyValue,
777    /// Actual value observed
778    pub actual_value: PropertyValue,
779    /// Deviation from expected
780    pub deviation: f64,
781}