Documentation
README
Abstract Invariant Generator
Overview
This skill uses abstract interpretation to automatically infer loop invariants, function preconditions, and postconditions. It generates formal specifications that support verification and reasoning about program correctness.
Invariant Generation Workflow
Step 1: Identify Specification Points
Analyze the code to identify where invariants are needed:
Loop Invariants: For each loop
while condition:
# Need: invariant that holds before/after each iteration
body
Function Contracts: For each function
def function(params):
# Need: precondition (what must be true on entry)
body
# Need: postcondition (what is guaranteed on exit)
This is the opening of the README. Read the full README on GitHub.