diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-18 17:19:18 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-18 17:19:18 -0700 |
| commit | 4baa0fad00861977f7ab9b11161adb1cb0d691cf (patch) | |
| tree | 323339486f58c4117ef5f1e0b6b2f45ec5b1cdf5 /Test | |
| parent | 0d02c233dc44f763911cfe7daeb0cb0c7a2ec624 (diff) | |
Dafny: added set comprehension expressions
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 13 | ||||
| -rw-r--r-- | Test/dafny0/Comprehensions.dfy | 40 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 1 |
3 files changed, 54 insertions, 0 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 2463b0e5..34aea30b 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -527,6 +527,19 @@ Execution trace: Dafny program verifier finished with 2 verified, 1 error
+-------------------- Comprehensions.dfy --------------------
+Comprehensions.dfy(9,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon9_Then
+ (0,0): anon10_Then
+ (0,0): anon4
+ (0,0): anon11_Then
+ (0,0): anon12_Then
+ (0,0): anon8
+
+Dafny program verifier finished with 6 verified, 1 error
+
-------------------- Termination.dfy --------------------
Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy new file mode 100644 index 00000000..8629a418 --- /dev/null +++ b/Test/dafny0/Comprehensions.dfy @@ -0,0 +1,40 @@ +method M()
+{
+ var numbers := set i | 0 <= i && i < 100;
+ var squares := set i | 0 <= i && i < 100 :: Id(i)*i; // verifying properties about set comprehensions with a term expression is hard
+
+ assert 12 in numbers;
+ assert Id(5) == 5;
+ assert 25 in squares;
+ assert 200 in numbers; // error
+}
+
+function method Id(x: int): int { x } // for triggering
+
+// The following mainly test that set comprehensions can be compiled, but one would
+// have to run the resulting program to check that the compiler is doing the right thing.
+method Main()
+{
+ var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;
+ call PrintSet(q);
+ q := set b: bool | true :: if b then 3 else 7;
+ call PrintSet(q);
+ var m := set k | k in q :: 2*k;
+ call PrintSet(m);
+ call PrintSet(set k | k in q && k % 2 == 0);
+ var sq := [30, 40, 20];
+ call PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
+ var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;
+}
+
+method PrintSet<T>(s: set<T>) {
+ var q := s;
+ while (q != {})
+ decreases q;
+ {
+ var x := choose q;
+ print x, " ";
+ q := q - {x};
+ }
+ print "\n";
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 12d9bcf4..f67429d2 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -15,6 +15,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy FunctionSpecifications.dfy ResolutionErrors.dfy
Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy
Modules0.dfy Modules1.dfy BadFunction.dfy
+ Comprehensions.dfy
Termination.dfy Use.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
Refinement.dfy RefinementErrors.dfy) do (
|