Cpp To Dafny Translator

C/C++ to Dafny Translator

Translate C/C++ programs into equivalent, verifiable Dafny code while preserving program semantics and ensuring memory safety.

Overview

This skill provides systematic guidance for translating C/C++ code to Dafny, handling memory management, pointer semantics, type conversions, and ensuring well-typed, verifiable output with appropriate specifications.

Translation Workflow

C/C++ Input → Analyze Structure → Map Types & Memory → Translate → Add Specifications → Verify
    ├─ Identify types, pointers, memory patterns
    ├─ Map C/C++ constructs to Dafny equivalents
    ├─ Handle memory safety and ownership
    ├─ Add preconditions, postconditions, invariants
    └─ Validate executability and verification

Core Translation Principles

1. Memory Safety First

Dafny enforces memory safety. Every translation must:

• Replace raw pointers with safe references or arrays
• Make memory bounds explicit
• Ensure no null pointer dereferences
• Handle dynamic memory with sequences or arrays

2. Preserve Semantics

The translated code must maintain the same computational behavior, preserve function contracts, keep algorithmic complexity, and handle all edge cases including error conditions.

3. Enable Verification

Generated Dafny code must include specifications (preconditions, postconditions, invariants), be verifiable by Dafny's verifier, compile and execute correctly, and follow Dafny idioms.

Type Mapping Reference

Basic Types

| C/C++ Type | Dafny Type | Notes | |-----------|-----------|-------| | int, long | int | Unbounded integers in Dafny | | unsigned int | nat | Natural numbers (≥ 0) | | char | char | Single character | | bool | bool | Direct mapping | | float, double | real | Exact rationals in Dafny | | void | () | Unit type | | NULL | Use Option or bounds checks | No null pointers |

Composite Types

| C/C++ Type | Dafny Type | Notes | |-----------|-----------|-------| | int arr[] | array | Fixed-size arrays | | int* ptr | array or seq | Depends on usage | | struct | class or datatype | Mutable vs immutable | | enum | datatype | Algebraic data types | | union | datatype with variants | Tagged unions |

For detailed mappings, see [references/typemappings.md](references/typemappings.md).

Translation Patterns

Functions

Simple C function:

int add(int a, int b) {
    return a + b;
}

Dafny:

function add(a: int, b: int): int
{
    a + b
}

Function with side effects:

void increment(int* x) {
    (*x)++;
}

Dafny (using method):

method increment(x: array, index: nat)
    requires index ) returns (sum: int)
    ensures sum == arraySum(arr[..])
{
    sum := 0;
    var i := 0;
    while i ): int
{
    if |s| == 0 then 0 else s[0] + arraySum(s[1..])
}

Structs and Classes

C struct:

struct Point {
    int x;
    int y;
};

int distance_squared(struct Point* p) {
    return p->x * p->x + p->y * p->y;
}

Dafny:

class Point {
    var x: int
    var y: int

    constructor(x0: int, y0: int)
        ensures x == x0 && y == y0
    {
        x := x0;
        y := y0;
    }
}

function distanceSquared(p: Point): int
    reads p
{
    p.x * p.x + p.y * p.y
}

Control Flow

If-else:

int max(int a, int b) {
    if (a > b) return a;
    else return b;
}

Dafny:

function max(a: int, b: int): int
{
    if a > b then a else b
}

Loops with invariants:

int factorial(int n) {
    int result = 1;
    for (int i = 1; i , target: int) returns (index: int)
    ensures index == -1 || (0 , target: int) returns (index: int)
    requires forall i, j :: 0  arr[i]  arr[i]  arr[i] > target
    {
        var mid := (low + high) / 2;
        if arr[mid]  target {
            high := mid;
        } else {
            return mid;
        }
    }
    return -1;
}

Translation Process

Step 1: Analyze C/C++ Code

Identify all functions, structs, and global variables. Analyze pointer usage and memory patterns. Identify side effects and state modifications. Note any unsafe operations.

Step 2: Plan Type and Memory Mappings

Map C/C++ types to Dafny types. Decide how to handle pointers (arrays, sequences, or references). Plan struct translations (class vs datatype). Identify what needs specifications.

Step 3: Translate Constructs

Start with data structures (structs → classes/datatypes). Translate pure functions first. Convert functions with side effects to methods. Add memory safety checks. Include necessary specifications.

Step 4: Add Verification Annotations

Add preconditions (requires). Add postconditions (ensures). Add loop invariants. Add frame conditions (reads, modifies). Add termination measures (decreases).

Step 5: Verify and Test

Run Dafny verifier. Fix verification errors. Test with concrete examples. Ensure executability.

Example Translation

C code:

int is_sorted(int* arr, int n) {
    for (int i = 0; i  arr[i + 1]) {
            return 0;
        }
    }
    return 1;
}

void bubble_sort(int* arr, int n) {
    for (int i = 0; i  arr[j + 1]) {
                int temp = arr[j];
                arr[j] = arr[j + 1];
                arr[j + 1] = temp;
            }
        }
    }
}

Dafny:

predicate isSorted(arr: array)
    reads arr
{
    forall i, j :: 0  arr[i] )
    modifies arr
    ensures isSorted(arr)
    ensures multiset(arr[..]) == multiset(old(arr[..]))
{
    var i := 0;
    while i  arr[k]  arr[k]  arr[j + 1] {
                arr[j], arr[j + 1] := arr[j + 1], arr[j];
            }
            j := j + 1;
        }
        i := i + 1;
    }
}

Best Practices

1. Start with Pure Functions: Translate side-effect-free code first
2. Add Specifications Incrementally: Start with simple contracts, refine as needed
3. Use Helper Functions: Define pure functions to express properties
4. Leverage Dafny's Verifier: Let the verifier guide you to correct specifications
5. Test Executability: Use Main methods to test concrete examples
6. Document Assumptions: Note where C semantics differ from Dafny
7. Handle Memory Explicitly: Make all memory bounds and ownership clear

Verification Checklist

Before finalizing translation:

• [ ] All types are correctly mapped
• [ ] Code compiles without errors
• [ ] Dafny verifier succeeds
• [ ] Preconditions capture all assumptions
• [ ] Postconditions specify all guarantees
• [ ] Loop invariants are sufficient for verification
• [ ] Memory safety is ensured (no out-of-bounds access)
• [ ] Termination is proven (decreases clauses if needed)
• [ ] Code is executable and produces correct results

Additional Resources

For complex translations, refer to:

• [Type Mappings](references/type_mappings.md) - Comprehensive C/C++ to Dafny type guide
• [Memory Patterns](references/memory_patterns.md) - Handling pointers, arrays, and dynamic memory
• [Verification Guide](references/verification_guide.md) - Writing effective specifications

Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: ArabelaTso
• Source: ArabelaTso/Skills-4-SE
• License: Apache-2.0
• Homepage: https://ArabelaTso.github.io/Skills-4-SE/

Install and usage instructions live in the source repository linked above.