I am struggling with Dafny’s syntax, and I get an error that I don’t know how to deal with. Here is the code:

function pow(base: int, exp: nat): int {
    if exp == 0 then 1 else base * pow(base, exp - 1)
}

method reversing(n: nat) returns (m: nat)
  requires n == sum(i: int | 0 <= i <= k :: c[i] * pow(10, i)) 
  ensures m == sum(i: int | 0 <= i <= k :: c[i] * pow(10, k-i)) 
{
  m := 0;
  var p := 0;
  while n > 0
    invariant m == sum(i: int | 0 <= i < p :: c[i] * pow(10, p-1-i))
    invariant n == sum(i: int | p <= i <= k :: c[i] * pow(10, i-p)) 
    decreases n 
  {
    p := p + 1;
    m := m * 10 + n % 10;
    n := n / 10;
  }
}

The method should return the reversing order of digits of a natural number saved in m. I get the same error at the precondition, postcondition and at the invariants: “closeparen expected”. What should I do and what does that mean?

I looked for other responses on the internet for this error but I didn’t find a response. I expect to get a useful alternative or at least an explanation for my issue.