Add test cases for property syntax #711

This adds a bunch of test cases (which currently fail) that use the new
property syntax.  Actually, the use of properties in the test cases
looks very nice.

misc/emacs/whiley.el

@@ -34,7 +34,7 @@ For detail, see `comment-dwim'."
      (comment-dwim arg)))
 
 (defvar whiley-keywords
-  '("native" "export" "extern" "null" "return" "if" "is" "throw" "throws" "try" "catch" "switch" "case" "default" "break" "continue" "skip" "do" "while" "for" "else" "define" "assume" "assert" "assume" "package" "import" "function" "method" "type" "constant" "from" "debug" "where" "ensures" "requires" "public" "protected" "private" "this" "str" "new" "in" "no" "some" "all" "false" "true")
+  '("native" "export" "extern" "null" "return" "if" "is" "throw" "throws" "try" "catch" "switch" "case" "default" "break" "continue" "skip" "do" "while" "for" "else" "define" "assume" "assert" "assume" "package" "import" "function" "method" "type" "constant" "from" "debug" "where" "ensures" "requires" "public" "protected" "private" "this" "str" "new" "in" "no" "some" "all" "false" "true" "property")
     "Whiley keywords.")
 
 (defvar whiley-types

tests/invalid/Property_Invalid_1.whiley

@@ -0,0 +1,11 @@
+property nat(int x) where x > 0
+
+function abs(int x) -> (int y)
+ensures nat(y)
+ensures (x == y) || (x == -y):
+    //
+    if x >= 0:
+        return x
+    else:
+        return y
+

tests/invalid/Property_Invalid_2.whiley

@@ -0,0 +1,8 @@
+property nat_a(int x) where x >= 0
+property nat_b(int x) where x > 0
+
+function id(int x) -> (int y)
+requires nat_a(x)
+ensures nat_b(x):
+    return x
+

tests/invalid/Property_Invalid_3.whiley

@@ -0,0 +1,8 @@
+property nat(int x) where x >= 0
+
+property natArray(int[] xs)
+where all { i in 0..|xs| | nat(xs[i]) }
+
+function id(int[] xs) -> (int[] ys)
+ensures natArray(ys):
+    return xs

tests/invalid/Property_Invalid_4.whiley

@@ -0,0 +1,8 @@
+property contains(int[] xs, int x)
+where some { i in 0..|xs| | xs[i] == x }
+
+function id(int[] xs, int x, int y) -> (int[] ys)
+requires contains(xs,y)
+ensures contains(ys,x):
+    return xs
+

tests/invalid/Property_Invalid_5.whiley

@@ -0,0 +1,24 @@
+type nat is (int x) where x >= 0
+
+property absent(int[] items, int item, int end)
+where all { i in 0..end | items[i] != item }
+
+function indexOf(int[] items, int item) -> (int r)
+ensures (r >= 0) ==> (items[r] == item)
+ensures (r < 0) ==> absent(items,item,|items|)
+    //
+    nat i = 0
+    //
+    while i < |items| where absent(items,item,i):
+        if items[i] == 0:
+            return i
+        i = i + 1
+    //
+    return -1
+
+public export method test():
+    int[] items = [4,3,1,5,4]
+    assume indexOf(items,0) == -1
+    assume indexOf(items,1) == 2
+    assume indexOf(items,4) == 0
+

tests/invalid/Property_Invalid_6.whiley

@@ -0,0 +1,27 @@
+type nat is (int x) where x >= 0
+
+property absent(int[] items, int item, int end)
+where all { i in 0..end | items[i] != item }
+
+property absent(int[] items, int item)
+where absert(items,item,|items|-1)
+
+function indexOf(int[] items, int item) -> (int r)
+ensures (r >= 0) ==> (items[r] == item)
+ensures (r < 0) ==> absent(items,item)
+    //
+    nat i = 0
+    //
+    while i < |items| where absent(items,item,i):
+        if items[i] == item:
+            return i
+        i = i + 1
+    //
+    return -1
+
+public export method test():
+    int[] items = [4,3,1,5,4]
+    assume indexOf(items,0) == -1
+    assume indexOf(items,1) == 2
+    assume indexOf(items,4) == 0
+

tests/invalid/Property_Invalid_7.whiley

@@ -0,0 +1,30 @@
+type nat is (int x) where x >= 0
+
+property max(int[] xs, int max, int n)
+// Max is not smaller than everything upto n
+where all { i in 0 .. n | max >= xs[i] }
+// Max is one of the values upto n
+where some { i in 0..n | max == xs[i] }
+
+// Determine the maximum value of an integer array
+function max(int[] items) -> (int r)
+// Input array cannot be empty
+requires |items| > 0
+// Return is max over all items
+ensures max(items,r,|items|)
+    //
+    nat i = 1
+    int m = items[0]
+    //
+    while i < |items| where max(items,m,m):
+        if items[i] > m:
+            m = items[i]
+        i = i + 1
+    //
+    return m
+
+public export method test():
+    int[] items = [4,3,1,5,4]
+    assume max([1,2,3]) == 3
+    assume max([4,3,1,5,4]) == 5
+

tests/invalid/Property_Invalid_8.whiley

@@ -0,0 +1,11 @@
+property nat(int x) where x >= 0
+property pos(int x) where x > 0
+
+type nat is (int x) where nat(x)
+type pos is (int x) where pos(x)
+
+function f1(pos x) -> (nat y):
+    return x
+
+function f2(nat x) -> (pos y):
+    return x

tests/valid/Property_Valid_1.whiley

@@ -0,0 +1,18 @@
+property nat(int x) where x >= 0
+
+function abs(int x) -> (int y)
+ensures nat(y)
+ensures (x == y) || (x == -y):
+    //
+    if x >= 0:
+        return x
+    else:
+        return y
+
+public export method test():
+    assert abs(-1) == 1
+    assert abs(-2) == 2
+    assert abs(0) == 0
+    assert abs(1) == 1
+    assert abs(2) == 2
+

tests/valid/Property_Valid_2.whiley

@@ -0,0 +1,15 @@
+property nat_a(int x) where x >= 0
+property nat_b(int x) where x >= 0
+
+function id(int x) -> (int y)
+requires nat_a(x)
+ensures nat_b(x):
+    return x
+
+
+public export method test():
+    assume id(-1) == -1
+    assume id(0) == 0
+    assume id(1) == 1
+    assume id(2) == 2
+

tests/valid/Property_Valid_3.whiley

@@ -0,0 +1,15 @@
+property nat(int x) where x >= 0
+
+property natArray(int[] xs)
+where all { i in 0..|xs| | nat(xs[i]) }
+
+function id(int[] xs) -> (int[] ys)
+requires natArray(xs)
+ensures natArray(ys):
+    return xs
+
+
+public export method test():
+    assume id([0]) == [0]
+    assume id([1,2]) == [1,2]
+    assume id([1,2,3]) == [1,2,3]

tests/valid/Property_Valid_4.whiley

@@ -0,0 +1,16 @@
+property contains(int[] xs, int x)
+where some { i in 0..|xs| | xs[i] == x }
+
+function id(int[] xs, int x) -> (int[] ys)
+requires contains(xs,x)
+ensures contains(ys,x):
+    return xs
+
+public export method test():
+    assume id([0],0) == [0]
+    assume id([1,2],1) == [1,2]
+    assume id([1,2],2) == [1,2]    
+    assume id([1,2,3],1) == [1,2,3]
+    assume id([1,2,3],2) == [1,2,3]
+    assume id([1,2,3],3) == [1,2,3]
+

tests/valid/Property_Valid_5.whiley

@@ -0,0 +1,24 @@
+type nat is (int x) where x >= 0
+
+property absent(int[] items, int item, int end)
+where all { i in 0..end | items[i] != item }
+
+function indexOf(int[] items, int item) -> (int r)
+ensures (r >= 0) ==> (items[r] == item)
+ensures (r < 0) ==> absent(items,item,|items|)
+    //
+    nat i = 0
+    //
+    while i < |items| where absent(items,item,i):
+        if items[i] == item:
+            return i
+        i = i + 1
+    //
+    return -1
+
+public export method test():
+    int[] items = [4,3,1,5,4]
+    assume indexOf(items,0) == -1
+    assume indexOf(items,1) == 2
+    assume indexOf(items,4) == 0
+

tests/valid/Property_Valid_6.whiley

@@ -0,0 +1,27 @@
+type nat is (int x) where x >= 0
+
+property absent(int[] items, int item, int end)
+where all { i in 0..end | items[i] != item }
+
+property absent(int[] items, int item)
+where absert(items,item,|items|)
+
+function indexOf(int[] items, int item) -> (int r)
+ensures (r >= 0) ==> (items[r] == item)
+ensures (r < 0) ==> absent(items,item)
+    //
+    nat i = 0
+    //
+    while i < |items| where absent(items,item,i):
+        if items[i] == item:
+            return i
+        i = i + 1
+    //
+    return -1
+
+public export method test():
+    int[] items = [4,3,1,5,4]
+    assume indexOf(items,0) == -1
+    assume indexOf(items,1) == 2
+    assume indexOf(items,4) == 0
+

tests/valid/Property_Valid_7.whiley

@@ -0,0 +1,30 @@
+type nat is (int x) where x >= 0
+
+property max(int[] xs, int max, int n)
+// Max is not smaller than everything upto n
+where all { i in 0 .. n | max >= xs[i] }
+// Max is one of the values upto n
+where some { i in 0..n | max == xs[i] }
+
+// Determine the maximum value of an integer array
+function max(int[] items) -> (int r)
+// Input array cannot be empty
+requires |items| > 0
+// Return is max over all items
+ensures max(items,r,|items|)
+    //
+    nat i = 1
+    int m = items[0]
+    //
+    while i < |items| where max(items,m,i):
+        if items[i] > m:
+            m = items[i]
+        i = i + 1
+    //
+    return m
+
+public export method test():
+    int[] items = [4,3,1,5,4]
+    assume max([1,2,3]) == 3
+    assume max([4,3,1,5,4]) == 5
+

tests/valid/Property_Valid_8.whiley

@@ -0,0 +1,12 @@
+property nat(int x) where x >= 0
+
+type nat is (int x) where nat(x)
+
+function id(nat x) -> (nat y):
+    return x
+
+public export method test():
+    assume id(-1) == -1
+    assume id(0) == 0
+    assume id(1) == 1
+    assume id(2) == 2