Dafny: Added if-then-else expressions (replacing and extending the previous boolean-only if-then-else expressions)

Dafny: Added 'class' functions and methods (i.e., functions and methods with a receiver parameter)
Dafny grammar changes:  Tthe 'use' keyword now goes before 'function' (akin to 'ghost' and 'class'), and quantifier triggers now go before the '::'
Dafny: Check for division-by-zero for both '/' and '%'

4 files changed, 67 insertions, 4 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 043a4cfd..d1584333 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -30,6 +30,21 @@ class MyClass<T, U> {
       assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];

     }

   }

+

+  function F(x: int, y: int, h: WildData, k: WildData): WildData

+  {

+    if x < 0 then

+      h

+    else if x == 0 then

+      if if h == k then true else false then

+        h

+      else if y == 0 then

+        k

+      else

+        h

+    else

+      k

+  }

 }

 

 datatype List<T> {

@@ -70,8 +85,25 @@ TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C
 SmallTests.dfy(30,7): Error: RHS expression must be well defined

 Execution trace:

     (0,0): anon0

+SmallTests.dfy(61,36): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Then

+SmallTests.dfy(62,51): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Else

+    (0,0): anon3

+    (0,0): anon11_Else

+SmallTests.dfy(63,22): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Then

+    (0,0): anon3

+    (0,0): anon11_Then

+    (0,0): anon6

 

-Dafny program verifier finished with 4 verified, 1 error

+Dafny program verifier finished with 6 verified, 4 errors

 

 -------------------- Queue.dfy --------------------

 

diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy
index a224ed91..c5599529 100644
--- a/Test/dafny0/Simple.dfy
+++ b/Test/dafny0/Simple.dfy
@@ -27,6 +27,14 @@ class MyClass<T,U> {
       assert v[x] != null ==> null !in v[2..x][1..][5 := v[this.x]][..10];

     }

   }

+

+  function F(x: int, y: int, h: WildData, k: WildData): WildData

+  {

+    if x < 0 then h else

+    if (x == 0) then

+      if if h==k then true else false then h else if y == 0 then k else h

+    else k

+  }

 }

 

 // some datatype stuff:

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 17f0168a..6ac9879d 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -43,4 +43,27 @@ class Node {
       t := s[..j] + [b] + s[j+1..];

     }

   }

+

+  method Max0(x: int, y: int) returns (r: int)

+    ensures r == (if x < y then y else x);

+  {

+    if (x < y) { r := y; } else { r := x; }

+  }

+

+  method Max1(x: int, y: int) returns (r: int)

+    ensures r == x || r == y;

+    ensures x <= r && y <= r;

+  {

+    r := if x < y then y else x;

+  }

+

+  function PoorlyDefined(x: int): int

+    requires if next == null then 5/x < 20 else true;  // ill-defined then branch

+    requires if next == null then true else 0 <= 5/x;  // ill-defined then branch

+    requires if next.next == null then true else true;  // ill-defined guard

+    requires 10/x != 8;  // this is well-defined, because we get here only if x is non-0

+    reads this;

+  {

+    12

+  }

 }

diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index 1d2d264f..8b7eafc1 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -1,7 +1,7 @@
 class T {

   var x: int;

 

-  function use F(y: int): int {

+  use function F(y: int): int {

     2*y

   }

 

@@ -12,7 +12,7 @@ class T {
     assert F(7) == 14;  // error (definition not engaged)

   }

 

-  function use G(y: int): bool {

+  use function G(y: int): bool {

     0 <= y

   }

 

@@ -25,7 +25,7 @@ class T {
     assert G(7);  // error (definition not engaged)

   }

 

-  function use H(): int

+  use function H(): int

     reads this;

   {

     x