Added types "char" and "string" (the latter being a synonym for "seq<char>").

Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings.
Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions.
Fixed lack of operator resolution in custom attributes.

1 files changed, 57 insertions, 0 deletions

diff --git a/Test/dafny0/Strings.dfy b/Test/dafny0/Strings.dfy
new file mode 100644
index 00000000..54764662
--- /dev/null
+++ b/Test/dafny0/Strings.dfy
@@ -0,0 +1,57 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%2.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+method Char(a: char, s: string, i: int) returns (b: char)

+{

+  var ch: char;

+  if a == ch {

+    b := ch;

+  } else if 0 <= i < |s| {

+    b := s[i];

+  }

+}

+

+// An attribute parameter that is a string literal is passed down

+// to Boogie as a string literal.

+method {:MyAttribute "hello", "hi" + "there", 57} AttrTest()

+{

+}

+

+method M(a: char, b: char) returns (s: string, t: seq<char>)

+  ensures |s| == 3 ==> t == [a, b, b];

+{

+  s := s + [a, b, b] + s;

+  t := s;

+  s := t[0..|s|];

+}

+

+method Main()

+{

+  var ch: char;

+  var s, t := M(ch, ch);

+  print "ch = ", ch, "\n";

+  print "The string is: " + s + "\n";

+  var x, y, z := Escapes();

+  print "Escape X: ", x, "\n";

+  print "Escape Y: ", y, "\n";

+  print "Escape Z: ", z, "\n";

+}

+

+method GimmieAChar(s: string) returns (ch: char)

+{

+  if s == "" {

+    ch := "tn"[1];

+    assert ch == "nt"[0];

+  } else {

+    var i :| 0 <= i < |s|;  // if guard guarantees such an i exists

+    ch := s[i];

+  }

+}

+

+method Escapes() returns (x: string, y: string, z: string)

+{

+  x := "I say \"hello\" \\ you say \'good bye'";

+  y := @"I say ""hello"" \ you say 'good bye'";

+  assert x == y;

+  z := "There needs to be \u0052\u0026\u0044\n\tYes, sir";

+}