Added a test case for <==.

2 files changed, 20 insertions, 10 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 42989a5a..26d4de73 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -879,11 +879,11 @@ Execution trace:
     (0,0): anon10

     Basics.dfy(66,95): anon18_Else

     (0,0): anon12

-Basics.dfy(100,16): Error: assertion violation

+Basics.dfy(110,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

-Basics.dfy(119,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must have the same value

+Basics.dfy(129,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must have the same value

 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

@@ -892,28 +892,28 @@ Execution trace:
     (0,0): anon6

     (0,0): anon12_Then

     (0,0): anon9

-Basics.dfy(133,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value

+Basics.dfy(143,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value

 Execution trace:

     (0,0): anon0

-Basics.dfy(145,19): Error: assertion violation

+Basics.dfy(155,19): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon11_Then

-Basics.dfy(147,10): Error: target object may be null

+Basics.dfy(157,10): Error: target object may be null

 Execution trace:

     (0,0): anon0

     (0,0): anon3

-Basics.dfy(147,10): Error: assignment may update an object not in the enclosing context's modifies clause

+Basics.dfy(157,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(152,12): Error: left-hand sides 0 and 1 may refer to the same location

+Basics.dfy(162,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(163,15): Error: assertion violation

+Basics.dfy(173,15): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon11_Then

@@ -923,11 +923,11 @@ Execution trace:
     (0,0): anon13_Then

     (0,0): anon8

     (0,0): anon14_Then

-Basics.dfy(226,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value

+Basics.dfy(236,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 32 verified, 11 errors

+Dafny program verifier finished with 34 verified, 11 errors

 

 -------------------- ControlStructures.dfy --------------------

 ControlStructures.dfy(5,3): Error: missing case in case statement: Purple

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index 7fca7199..ccd55fa3 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -66,6 +66,16 @@ method ChallengeTruth(j: int, k: int)
   assert j <= j + k != k + j + 1 < k+k+j <=/*this is the error*/ j+j+k < k+k+j+j == 2*k + 2*j == 2*(k+j);

 }

 

+// ---------- reverse implication ------------------------------------

+

+method Explies(s: seq<int>, i: nat)

+  requires forall x :: x in s ==> x > 0;

+{

+  var a, b, c: bool;

+  assert a <== b <== c <== false;   // OK, because <== is left-associative

+  assert s[i] > 0 <== i < |s|;      // OK, because <== is short-circuiting from the right

+}

+

 // --------- multi assignments --------------------------------

 

 class Multi {