begriffs open source - acsl-example/blob - CLAUDE.md

   1 # CLAUDE.md
   2
   3 This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.
   4
   5 ## Project Overview
   6
   7 This is an ACSL (ANSI/ISO C Specification Language) formal verification project demonstrating array search algorithms with varying specification complexity. The project uses Frama-C with the WP plugin for automated proof verification.
   8
   9 ## Architecture
  10
  11 ### Header Organization
  12 The project uses a layered header architecture separating user-facing API from proof infrastructure:
  13
  14 - **`inc/types.h`** - Basic type definitions
  15 - **`inc/algos.h`** - Public API with function declarations
  16 - **`inc/proof/`** - Proof infrastructure (separate from user-facing API)
  17   - **`existence.h`** - Element existence predicates and lemmas
  18   - **`search.h`** - Logic functions with comprehensive lemmas
  19
  20 ### Selective Axiom Architecture
  21 Each source file includes only the axioms it needs for optimal verification performance. This design achieves both elegant organization and fast verification by avoiding unnecessary axiom verification overhead.
  22
  23 ## Build System
  24
  25 Uses Meson build system with custom Frama-C verification tests.
  26
  27 ### Build Commands
  28 ```bash
  29 meson setup build
  30 meson compile -C build
  31 ```
  32
  33 ### Testing Commands
  34 ```bash
  35 # Run all verification tests
  36 meson test -C build
  37
  38 # Run specific test by name
  39 meson test -C build [test_name]
  40
  41 # Verbose test output (shows detailed Frama-C profiling)
  42 meson test -C build --verbose
  43 ```
  44
  45 ### Performance Analysis
  46 The verbose test output provides detailed profiling information including individual proof goal timing, timeout identification, prover statistics, and total verification time. Use this for identifying performance bottlenecks.
  47
  48 ## Verification Details
  49
  50 ### ACSL Contracts
  51 Functions use ACSL contracts with varying levels of abstraction - from basic behavioral contracts with inline quantifiers to abstract logic functions. The choice depends on verification performance vs specification elegance trade-offs.
  52
  53 ### Frama-C Configuration
  54 Tests run with comprehensive verification flags: `-wp -wp-rte -wp-prover cvc4 -verbose 2 -wp-verbose 3 -wp-debug 1 -wp-proof-trace`
  55
  56 ## Development Workflow
  57
  58 When adding new algorithms or modifying specifications:
  59 1. Create source files with inline ACSL contracts
  60 2. Include appropriate headers from `inc/proof/` for needed axioms
  61 3. Update `meson.build` to add new test cases
  62 4. Run verification tests to ensure proofs pass
  63 5. Use verbose output to optimize performance if needed
  64 6. Never commit unless verification succeeds
  65
  66 The architecture prioritizes both mathematical elegance and verification performance through selective axiom inclusion.