C++ → Dafny Translator

This is a delta over → python-to-dafny-translator — the Dafny target is the same; the source is harder. C++ brings three problems Python doesn't: fixed-width integers (overflow), pointers (aliasing), and manual memory (lifetime).

The C++-specific impedance mismatch

The overflow question — decide upfront

This is the most important modeling choice:

Option A — Prove no overflow: Use Dafny int (unbounded). Add ensures result fits in int32. The proof obligation is that your arithmetic never exceeds bounds. This is what you want for verifying the algorithm is overflow-safe.

Option B — Model wraparound: Use bv32. Arithmetic wraps silently. Use this only if the C++ intentionally relies on wrap (hash functions, checksums).

Most of the time you want Option A. If Dafny refuses to verify because a + b might overflow — that's the bug you were looking for.

Pointer modeling

A C++ pointer int* p pointing into array arr at offset k becomes two Dafny variables:

var arr: array<int>;
var k: nat;               // requires k <= arr.Length
// *p       ↦  arr[k]
// p[i]     ↦  arr[k + i]    with proof obligation k + i < arr.Length
// p++      ↦  k := k + 1

Aliasing: if C++ has int* p, *q that might point into the same array, Dafny needs modifies clauses and frame reasoning. If they're known-disjoint, say so: requires arr_p != arr_q.

Worked example

C++:

// Returns index of minimum element, or -1 if empty
int argmin(const int* a, size_t n) {
    if (n == 0) return -1;
    size_t best = 0;
    for (size_t i = 1; i < n; ++i) {
        if (a[i] < a[best]) best = i;
    }
    return (int)best;    // UB if best > INT_MAX
}

Dafny:

method ArgMin(a: array<int>) returns (r: int)
  requires a.Length <= 0x7fffffff              // ← UB guard: result fits in int
  ensures a.Length == 0 ==> r == -1
  ensures a.Length > 0  ==>
          0 <= r < a.Length &&
          forall j :: 0 <= j < a.Length ==> a[r] <= a[j]
{
  if a.Length == 0 { return -1; }
  var best := 0;
  var i := 1;
  while i < a.Length
    invariant 1 <= i <= a.Length
    invariant 0 <= best < i
    invariant forall j :: 0 <= j < i ==> a[best] <= a[j]   // best is min of prefix
    decreases a.Length - i
  {
    if a[i] < a[best] { best := i; }
    i := i + 1;
  }
  return best;
}

Note the requires a.Length <= INT_MAX — this is the translation of the C++ cast's UB into an explicit precondition. If the caller can't prove it, the cast was a real bug.

What doesn't translate

Do not

• Do not use bv32 by default "because C++ ints are 32-bit." Use int and prove no-overflow — that's usually the property you want.
• Do not model every *p as arr[0]. The offset matters. p++; *p is arr[1], not arr[0].
• Do not drop const without thinking. C++ const int* means the function doesn't write through it — that's a frame condition: the array isn't in modifies.
• Do not pretend the cast away. (int)size_t_val has a precondition; state it.

Output format

Same as → python-to-dafny-translator, plus:

## Integer model
<int (prove-no-overflow) | bvN (model-wrap)> — <why>

## Pointer model
<pointer> ↦ (<array>, <index>)  — aliasing: <disjoint | may-alias>

## UB → preconditions
<each C++ UB that became a requires clause>