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, verifiable, and can successfully run.
Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.
A direct command skips the review prompt. Inspect the source before running it.
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, verifiable, and can successfully run.
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.
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.
intsum_array(int* arr, int n) {
int sum = 0;
for (int i = 0; i < n; i++) {
sum += arr[i];
}
return sum;
}
Dafny:
method sumArray(arr: array<int>) returns (sum: int)
ensures sum == arraySum(arr[..])
{
sum := 0;
var i := 0;
while i < arr.Length
invariant 0 <= i <= arr.Length
invariant sum == arraySum(arr[..i])
{
sum := sum + arr[i];
i := i + 1;
}
}
function arraySum(s: seq<int>): int
{
if |s| == 0 then 0 else s[0] + arraySum(s[1..])
}
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:
intmax(int a, int b) {
if (a > b) return a;
elsereturn b;
}
Dafny:
function max(a: int, b: int): int
{
if a > b then a else b
}
Loops with invariants:
intfactorial(int n) {
int result = 1;
for (int i = 1; i <= n; i++) {
result *= i;
}
return result;
}
Dafny:
method factorial(n: nat) returns (result: nat)
ensures result == fact(n)
{
result := 1;
var i := 1;
while i <= n
invariant 1 <= i <= n + 1
invariant result == fact(i - 1)
{
result := result * i;
i := i + 1;
}
}
function fact(n: nat): nat
{
if n == 0 then 1 else n * fact(n - 1)
}
Handling Common Challenges
1. Pointer Arithmetic
Challenge: C allows pointer arithmetic; Dafny doesn't.
Solution: Use array indices instead:
// Cint* ptr = arr + 5;
*ptr = 10;
// Dafny
arr[5] := 10;
2. Dynamic Memory Allocation
Challenge: C uses malloc/free; Dafny has automatic memory management.
// Dafny
var arr := new int[n];
// ... use arr ...
// No explicit free needed
3. Null Pointers
Challenge: C allows NULL; Dafny doesn't have null references.
Solution: Use Option types or ensure non-null:
// Cint* find(int* arr, int n, int target) {
for (int i = 0; i < n; i++) {
if (arr[i] == target) return &arr[i];
}
returnNULL;
}
// Dafny
method find(arr: array<int>, target: int) returns (index: int)
ensures index == -1 || (0 <= index < arr.Length && arr[index] == target)
{
var i := 0;
while i < arr.Length
invariant 0 <= i <= arr.Length
{
if arr[i] == target {
return i;
}
i := i + 1;
}
return -1;
}
4. Mutable vs Immutable
Challenge: C has mutable everything; Dafny distinguishes functions (pure) from methods (with side effects).
Solution:
Use function for pure computations
Use method for operations with side effects
Add reads clauses for functions that read object fields
Add modifies clauses for methods that modify state
5. Verification Annotations
Challenge: Dafny requires specifications for verification.
Solution: Add preconditions, postconditions, and loop invariants:
method binarySearch(arr: array<int>, target: int) returns (index: int)
requires forall i, j :: 0 <= i < j < arr.Length ==> arr[i] <= arr[j] // sorted
ensures index == -1 || (0 <= index < arr.Length && arr[index] == target)
{
var low := 0;
var high := arr.Length;
while low < high
invariant 0 <= low <= high <= arr.Length
invariant forall i :: 0 <= i < low ==> arr[i] < target
invariant forall i :: high <= i < arr.Length ==> arr[i] > target
{
var mid := (low + high) / 2;
if arr[mid] < target {
low := mid + 1;
} else 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.
