Some more test cases for associativity and short-circuitness of <==

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