From f7250b98f91a9e81069b0dc2c7b9c16b36633dfc Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Thu, 4 Feb 2010 22:14:26 +0000
Subject: 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 '%'

---
 Test/dafny0/Answer         | 34 +++++++++++++++++++++++++++++++++-
 Test/dafny0/Simple.dfy     |  8 ++++++++
 Test/dafny0/SmallTests.dfy | 23 +++++++++++++++++++++++
 Test/dafny0/Use.dfy        |  6 +++---
 4 files changed, 67 insertions(+), 4 deletions(-)

(limited to 'Test')

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
-- 
cgit v1.2.3