diff options
author | leino <unknown> | 2014-10-13 18:31:22 -0700 |
---|---|---|
committer | leino <unknown> | 2014-10-13 18:31:22 -0700 |
commit | 25491156486a9e1a1642278f40ea6e9378c72da7 (patch) | |
tree | 98f55cbdd7922f24a9ecb121ece57fddfbbfdbbc /Test | |
parent | 969ef55e0c579e0538eff680f8bbf1b289777500 (diff) |
Some more test cases for associativity and short-circuitness of <==
Diffstat (limited to 'Test')
-rw-r--r-- | Test/dafny0/Basics.dfy | 36 | ||||
-rw-r--r-- | Test/dafny0/Basics.dfy.expect | 76 |
2 files changed, 99 insertions, 13 deletions
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 946981ac..b639acc5 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -79,6 +79,42 @@ method Explies(s: seq<int>, i: nat) assert s[i] > 0 <== i < |s|; // OK, because <== is short-circuiting from the right
}
+method ExpliesAssociativityM(A: bool, B: bool, C: bool) {
+ var x := A ==> B;
+ var y := B <== A;
+ var z;
+ assert x == y;
+
+ if * {
+ x := A ==> B ==> C;
+ y := A ==> (B ==> C); // parens not needed, because ==> is right associative
+ z := (A ==> B) ==> C;
+ assert x == y;
+ assert x == z; // error
+ } else {
+ x := A <== B <== C;
+ y := (A <== B) <== C; // parens not needed, because <== is left associative
+ z := A <== (B <== C);
+ assert x == y;
+ assert x == z; // error
+ }
+}
+
+method ExpliesShortCircuiting(a: array<T>)
+{
+ assert a == null || 0 <= a.Length; // (W)
+ assert a != null ==> 0 <= a.Length; // (X) -- same as (W)
+ assert 0 <= a.Length <== a != null; // (Y)
+
+ // Note: short-circuiting is left-to-right for &&, ||, and ==>, but it is
+ // right-to-left for <==
+ if * {
+ assert a == null <== a.Length < 0; // error: contrapositive of (X), but not well-formed
+ } else {
+ assert a.Length < 0 ==> a == null; // error: contrapositive of (Y), but not well-formed
+ }
+}
+
// --------- multi assignments --------------------------------
class Multi {
diff --git a/Test/dafny0/Basics.dfy.expect b/Test/dafny0/Basics.dfy.expect index 5fccdb36..db074f4a 100644 --- a/Test/dafny0/Basics.dfy.expect +++ b/Test/dafny0/Basics.dfy.expect @@ -12,11 +12,61 @@ Execution trace: Basics.dfy(69,82): anon17_Else
Basics.dfy(69,95): anon18_Else
(0,0): anon12
-Basics.dfy(113,16): Error: assertion violation
+Basics.dfy(93,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Basics.dfy(83,14): anon27_Else
+ (0,0): anon2
+ Basics.dfy(84,14): anon28_Else
+ (0,0): anon4
+ (0,0): anon29_Then
+ Basics.dfy(89,12): anon30_Else
+ (0,0): anon8
+ Basics.dfy(90,12): anon32_Else
+ (0,0): anon11
+ Basics.dfy(91,13): anon34_Else
+ (0,0): anon35_Then
+ (0,0): anon15
+Basics.dfy(99,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Basics.dfy(83,14): anon27_Else
+ (0,0): anon2
+ Basics.dfy(84,14): anon28_Else
+ (0,0): anon4
+ (0,0): anon29_Else
+ Basics.dfy(95,18): anon36_Else
+ (0,0): anon19
+ Basics.dfy(96,20): anon38_Else
+ (0,0): anon22
+ Basics.dfy(97,19): anon40_Else
+ (0,0): anon41_Then
+ (0,0): anon26
+Basics.dfy(112,28): Error: target object may be null
+Execution trace:
+ (0,0): anon0
+ Basics.dfy(105,20): anon13_Else
+ (0,0): anon2
+ Basics.dfy(106,20): anon14_Else
+ (0,0): anon4
+ Basics.dfy(107,24): anon15_Else
+ (0,0): anon6
+ (0,0): anon16_Then
+Basics.dfy(114,14): Error: target object may be null
+Execution trace:
+ (0,0): anon0
+ Basics.dfy(105,20): anon13_Else
+ (0,0): anon2
+ Basics.dfy(106,20): anon14_Else
+ (0,0): anon4
+ Basics.dfy(107,24): anon15_Else
+ (0,0): anon6
+ (0,0): anon16_Else
+Basics.dfy(149,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon10_Then
-Basics.dfy(132,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value
+Basics.dfy(168,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
(0,0): anon10_Then
@@ -25,28 +75,28 @@ Execution trace: (0,0): anon6
(0,0): anon12_Then
(0,0): anon9
-Basics.dfy(146,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
+Basics.dfy(182,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
-Basics.dfy(158,19): Error: assertion violation
+Basics.dfy(194,19): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon11_Then
-Basics.dfy(160,10): Error: assignment may update an object not in the enclosing context's modifies clause
+Basics.dfy(196,10): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3
-Basics.dfy(160,10): Error: target object may be null
+Basics.dfy(196,10): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon3
-Basics.dfy(165,12): Error: left-hand sides 0 and 1 may refer to the same location
+Basics.dfy(201,12): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon11_Then
(0,0): anon3
(0,0): anon12_Then
-Basics.dfy(176,15): Error: assertion violation
+Basics.dfy(212,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon11_Then
@@ -56,22 +106,22 @@ Execution trace: (0,0): anon13_Then
(0,0): anon8
(0,0): anon14_Then
-Basics.dfy(238,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
+Basics.dfy(274,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
-Basics.dfy(429,12): Error: assertion violation
+Basics.dfy(465,12): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Basics.dfy(440,19): Error: assertion violation
+Basics.dfy(476,19): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Basics.dfy(442,12): Error: assertion violation
+Basics.dfy(478,12): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Dafny program verifier finished with 61 verified, 14 errors
+Dafny program verifier finished with 63 verified, 18 errors
|