diff options
author | leino <unknown> | 2014-10-20 18:42:33 -0700 |
---|---|---|
committer | leino <unknown> | 2014-10-20 18:42:33 -0700 |
commit | c182b533a83dfee69828620f12a051feaab03eac (patch) | |
tree | 6223081d1ca9009afb83f0ff44758a196f9cfce9 /Test | |
parent | 12242050fe7069f7dcf4e99f23b14f447e6b55e0 (diff) |
Add char literals.
Disallow backslash from being part of identifier names.
Diffstat (limited to 'Test')
-rw-r--r-- | Test/dafny0/Strings.dfy | 12 | ||||
-rw-r--r-- | Test/dafny0/Strings.dfy.expect | 4 |
2 files changed, 15 insertions, 1 deletions
diff --git a/Test/dafny0/Strings.dfy b/Test/dafny0/Strings.dfy index 54764662..f56f36e1 100644 --- a/Test/dafny0/Strings.dfy +++ b/Test/dafny0/Strings.dfy @@ -35,6 +35,8 @@ method Main() print "Escape X: ", x, "\n";
print "Escape Y: ", y, "\n";
print "Escape Z: ", z, "\n";
+ var c, d := CharEscapes();
+ print "Here is the end" + [c, d] + [' ', ' ', ' '] + [[d]][0] + " ", d, "\n";
}
method GimmieAChar(s: string) returns (ch: char)
@@ -55,3 +57,13 @@ method Escapes() returns (x: string, y: string, z: string) assert x == y;
z := "There needs to be \u0052\u0026\u0044\n\tYes, sir";
}
+
+method CharEscapes() returns (c: char, d: char)
+{
+ // cool variable names, huh?
+ var 'x := 'R';
+ var x' := '\u0052';
+ assert 'x==x' ;
+ c := '\n';
+ d := '*';
+}
diff --git a/Test/dafny0/Strings.dfy.expect b/Test/dafny0/Strings.dfy.expect index 56bffd98..e05312b7 100644 --- a/Test/dafny0/Strings.dfy.expect +++ b/Test/dafny0/Strings.dfy.expect @@ -1,5 +1,5 @@ -Dafny program verifier finished with 12 verified, 0 errors
+Dafny program verifier finished with 14 verified, 0 errors
Program compiled successfully
Running...
@@ -9,3 +9,5 @@ Escape X: I say "hello" \ you say 'good bye' Escape Y: I say "hello" \ you say 'good bye' Escape Z: There needs to be R&D Yes, sir +Here is the end +* * * |