Trait CodeGenerator 

pub trait CodeGenerator: Send + Sync {
    // Required methods
    fn generate(
        &self,
        program: &ProgramModel,
        invariants: &[Invariant],
    ) -> Result<GenerationOutput>;
    fn chain(&self) -> &str;
}

Generates instrumented code with invariant checks.

Implementations inject assertions after state mutations.

Required Methods

fn generate( &self, program: &ProgramModel, invariants: &[Invariant], ) -> Result<GenerationOutput>

Generate instrumented code.

Errors

Returns an error if:

• Invariant expressions reference undefined state
• Type mismatches are detected
• Code generation fails

fn chain(&self) -> &str

Chain identifier.

Implementors