diff options
| author |  leino <unknown> | 2015-10-03 02:40:41 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-10-03 02:40:41 -0700 |
| commit | e07d86d6cc4423703dbfb479f09b44c80f877ef9 (patch) | |
| tree | f2300210ce0d45f889108e149bbee7a45b401e54 /Test/dafny0 | |
| parent | cfe05df94a5ccb6025c94bd21b09bfc1240de756 (diff) | |
Parsing and pretty printing of the new "existential guards" of the two kinds of "if" statements.
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/ExistentialGuards.dfy | 89 | ||||
| -rw-r--r-- | Test/dafny0/ExistentialGuards.dfy.expect | 94 | ||||
| -rw-r--r-- | Test/dafny0/Simple.dfy | 27 | ||||
| -rw-r--r-- | Test/dafny0/Simple.dfy.expect | 29 |
4 files changed, 239 insertions, 0 deletions
diff --git a/Test/dafny0/ExistentialGuards.dfy b/Test/dafny0/ExistentialGuards.dfy new file mode 100644 index 00000000..001acb55 --- /dev/null +++ b/Test/dafny0/ExistentialGuards.dfy @@ -0,0 +1,89 @@ +// RUN: %dafny /dprint:- "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate P(n: int)
+
+predicate R(r: real)
+
+method M0()
+{
+ if x :| P(x) {
+ }
+}
+
+method M1()
+{
+ if x: int :| P(x) {
+ }
+}
+
+method M2()
+{
+ if x, y :| P(x) && R(y) {
+ }
+}
+
+method M3()
+{
+ if x: int, y :| P(x) && R(y) {
+ }
+}
+
+method M4()
+{
+ if x, y: real :| P(x) && R(y) {
+ }
+}
+
+method M5()
+{
+ if x: int, y: real :| P(x) && R(y) {
+ }
+}
+
+method M6()
+{
+ if x {:myattribute x, "hello"} :| P(x) {
+ }
+ if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
+ }
+ if x: int {:myattribute x, "chello"} :| P(x) {
+ }
+ if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
+ }
+}
+
+method M7()
+{
+ if x :| P(x) {
+ } else if * {
+ } else if y :| R(y) {
+ } else if y :| P(y) {
+ }
+}
+
+method P0(m: int, n: int)
+ requires m < n
+{
+ if {
+ case x :| P(x) =>
+ case x: int :| P(x) =>
+ case x, y :| P(x) && R(y) =>
+ case x: int, y :| P(x) && R(y) =>
+ case m < n => // just to be different
+ case x, y: real :| P(x) && R(y) =>
+ case x: int, y: real :| P(x) && R(y) =>
+ }
+}
+
+method P1(m: int, n: int)
+ requires m < n
+{
+ if {
+ case x {:myattribute x, "hello"} :| P(x) =>
+ case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>
+ case x: int {:myattribute x, "chello"} :| P(x) =>
+ case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>
+ case m < n =>
+ }
+}
diff --git a/Test/dafny0/ExistentialGuards.dfy.expect b/Test/dafny0/ExistentialGuards.dfy.expect new file mode 100644 index 00000000..cf229553 --- /dev/null +++ b/Test/dafny0/ExistentialGuards.dfy.expect @@ -0,0 +1,94 @@ +// Dafny program verifier version 1.9.5.20511, Copyright (c) 2003-2015, Microsoft.
+// Command Line Options: -nologo -countVerificationErrors:0 -useBaseNameForFileName /dprint:- C:\dafny\Test\dafny0\ExistentialGuards.dfy
+// ExistentialGuards.dfy
+
+predicate P(n: int)
+
+predicate R(r: real)
+
+method M0()
+{
+ if x :| P(x) {
+ }
+}
+
+method M1()
+{
+ if x: int :| P(x) {
+ }
+}
+
+method M2()
+{
+ if x, y :| P(x) && R(y) {
+ }
+}
+
+method M3()
+{
+ if x: int, y :| P(x) && R(y) {
+ }
+}
+
+method M4()
+{
+ if x, y: real :| P(x) && R(y) {
+ }
+}
+
+method M5()
+{
+ if x: int, y: real :| P(x) && R(y) {
+ }
+}
+
+method M6()
+{
+ if x {:myattribute x, "hello"} :| P(x) {
+ }
+ if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
+ }
+ if x: int {:myattribute x, "chello"} :| P(x) {
+ }
+ if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
+ }
+}
+
+method M7()
+{
+ if x :| P(x) {
+ } else if * {
+ } else if y :| R(y) {
+ } else if y :| P(y) {
+ }
+}
+
+method P0(m: int, n: int)
+ requires m < n
+{
+ if {
+ case x :| P(x) =>
+ case x: int :| P(x) =>
+ case x, y :| P(x) && R(y) =>
+ case x: int, y :| P(x) && R(y) =>
+ case m < n =>
+ case x, y: real :| P(x) && R(y) =>
+ case x: int, y: real :| P(x) && R(y) =>
+ }
+}
+
+method P1(m: int, n: int)
+ requires m < n
+{
+ if {
+ case x {:myattribute x, "hello"} :| P(x) =>
+ case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>
+ case x: int {:myattribute x, "chello"} :| P(x) =>
+ case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>
+ case m < n =>
+ }
+}
+
+Dafny program verifier finished with 22 verified, 0 errors
+Compilation error: Function _module._default.P has no body
+Compilation error: Function _module._default.R has no body
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index f7bfcb70..0b6a620e 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -74,3 +74,30 @@ class CF { static protected function method I(): real
protected static predicate method J()
}
+
+// test printing of various if statements, including with omitted guards
+module A {
+ method P(x: int, y: int) {
+ if x==2 {
+ } else if * {
+ }
+ if x==10 {
+ }
+ if y==0 {
+ } else if y==1 {
+ } else if * {
+ } else if y==2 {
+ } else if (*) {
+ } else if y == 3 {
+ } else {
+ }
+ }
+}
+module B refines A {
+ method P... {
+ if ... {
+ } else if x==3 {
+ }
+ ...;
+ }
+}
diff --git a/Test/dafny0/Simple.dfy.expect b/Test/dafny0/Simple.dfy.expect index e6647c8a..d5eb6722 100644 --- a/Test/dafny0/Simple.dfy.expect +++ b/Test/dafny0/Simple.dfy.expect @@ -67,6 +67,35 @@ class CF { static protected predicate method J()
}
+module A {
+ method P(x: int, y: int)
+ {
+ if x == 2 {
+ } else if * {
+ }
+ if x == 10 {
+ }
+ if y == 0 {
+ } else if y == 1 {
+ } else if * {
+ } else if y == 2 {
+ } else if * {
+ } else if y == 3 {
+ } else {
+ }
+ }
+}
+
+module B refines A {
+ method P ...
+ {
+ if ... {
+ } else if x == 3 {
+ }
+ ...;
+ }
+}
+
lemma M(x: int)
ensures x < 8
{
|