# Cpp To Dafny Translator

> Translate C/C++ programs to equivalent Dafny code while preserving semantics and ensuring verification. Use when users ask to convert, translate, or port C/C++ code to Dafny, or when they need to formally verify C/C++ algorithms using Dafny's verification capabilities. Handles functions, structs, pointers, arrays, memory management, and ensures the generated Dafny code is well-typed, executable,…

- **Type:** Skill
- **Install:** `agentstack add skill-arabelatso-skills-4-se-cpp-to-dafny-translator`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [ArabelaTso](https://agentstack.voostack.com/s/arabelatso)
- **Installs:** 0
- **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills)
- **Latest version:** 0.1.0
- **License:** Apache-2.0
- **Upstream author:** [ArabelaTso](https://github.com/ArabelaTso)
- **Source:** https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/cpp-to-dafny-translator
- **Website:** https://ArabelaTso.github.io/Skills-4-SE/

## Install

```sh
agentstack add skill-arabelatso-skills-4-se-cpp-to-dafny-translator
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# 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/type_mappings.md](references/type_mappings.md).

## Translation Patterns

### Functions

**Simple C function:**
```c
int add(int a, int b) {
    return a + b;
}
```

**Dafny:**
```dafny
function add(a: int, b: int): int
{
    a + b
}
```

**Function with side effects:**
```c
void increment(int* x) {
    (*x)++;
}
```

**Dafny (using method):**
```dafny
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:**
```c
struct Point {
    int x;
    int y;
};

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

**Dafny:**
```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:**
```c
int max(int a, int b) {
    if (a > b) return a;
    else return b;
}
```

**Dafny:**
```dafny
function max(a: int, b: int): int
{
    if a > b then a else b
}
```

**Loops with invariants:**
```c
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:**
```c
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:**
```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](https://github.com/ArabelaTso)
- **Source:** [ArabelaTso/Skills-4-SE](https://github.com/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.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-arabelatso-skills-4-se-cpp-to-dafny-translator
- Seller: https://agentstack.voostack.com/s/arabelatso
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.