Convert numbers to strings

user_1979914 0
Viewed 143

I am trying to write a function which takes in val:nat, votes: set<nat>, N: nat where N is the maximum size of the set, votes, and returns a string which concatenates the val and votes.

Example: H(val: 23, votes:{1,3}, N: 3) will return "23-1-0-3"

Any leads is appreciated. Thanks.

dafny
2 Answers

There's no built-in conversion of numbers to strings. You can write a function to do it. (If you do, you're welcome to file a Pull Request on the under-utilized https://github.com/dafny-lang/libraries.)

Note, if you only need to print the number, you can do that with the print statement.

user_34344870

You can use the following conversion from nat to string, which has the feature that it's proven in both sides. You can safely use Printer.natToString in contexts where you only expects a string, as it provides more guarantee about this string than you would need though.
I used {:options "/functionSyntax:4"} so that the functions below are compilable without using the "method" keyword.

module {:options "/functionSyntax:4"} Printer {

  type stringNat = s: string |
    |s| > 0 && (|s| > 1 ==> s[0] != '0') &&
    forall i | 0 <= i < |s| :: s[i] in "0123456789"
    witness "1"

  function natToString(n: nat): stringNat {
    match n
    case 0 => "0" case 1 => "1" case 2 => "2" case 3 => "3" case 4 => "4"
    case 5 => "5" case 6 => "6" case 7 => "7" case 8 => "8" case 9 => "9"
    case _ => natToString(n / 10) + natToString(n % 10)
  }

  function stringToNat(s: stringNat): nat
    decreases |s|
  {
    if |s| == 1 then
      match s[0]
      case '0' => 0 case '1' => 1 case '2' => 2 case '3' => 3 case '4' => 4
      case '5' => 5 case '6' => 6 case '7' => 7 case '8' => 8 case '9' => 9
    else
      stringToNat(s[..|s|-1])*10 + stringToNat(s[|s|-1..|s|])
  }

  lemma natToStringThenStringToNatIdem(n: nat)
    ensures stringToNat(natToString(n)) == n
  { // Proof is automatic
  }
  lemma stringToNatThenNatToStringIdem(n: stringNat)
    ensures natToString(stringToNat(n)) == n
  { // Proof is automatic
  }
}
user_12878560
Related