From 55e161b62479ee1a3ff8d49d927dd4b35083fe6a Mon Sep 17 00:00:00 2001
From: Bart Wijgers <bartwijgers@hotmail.com>
Date: Fri, 27 Sep 2019 16:11:19 +0200
Subject: [PATCH] Update examples
Some examples had syntax errors; those have been fixed. Additionally,
I added a simple example with a while loop. It does not contain a proper
post-condition either, which might be interesting as well (as the
program might be able to handle those properly too).
---
examples/abs | 2 +-
examples/memberOf | 4 ++--
examples/sumArray | 12 ++++++++++++
3 files changed, 15 insertions(+), 3 deletions(-)
create mode 100644 examples/sumArray
diff --git a/examples/abs b/examples/abs
index 85e39d7..6830938 100644
--- a/examples/abs
+++ b/examples/abs
@@ -1,6 +1,6 @@
abs ( x : int | y : int ) {
assume x > 0;
- if x[ 0 ] < 0 then y := 0 else skip ;
+ if x < 0 then { y := 0 } else { skip; skip; skip; skip } ;
assert y > 0
}
diff --git a/examples/memberOf b/examples/memberOf
index 624fa14..d137deb 100644
--- a/examples/memberOf
+++ b/examples/memberOf
@@ -5,9 +5,9 @@ memberOf ( x : int , a :[] int | found : bool ) {
k := 0 ;
found := false ;
while k <# a do {
- if a [ k ]= x then found := true else skip ;
+ if a [ k ]= x then { found := true } else { skip } ;
k := k +1
}
};
assert found
-}
\ No newline at end of file
+}
diff --git a/examples/sumArray b/examples/sumArray
new file mode 100644
index 0000000..607323c
--- /dev/null
+++ b/examples/sumArray
@@ -0,0 +1,12 @@
+sumArray(arr: []int, first: int, last: int | sum: int) {
+ assume (first >= 0 && last < #arr && first < last);
+ sum := 0;
+ current := first;
+
+ while (current <= last) do {
+ sum := sum + arr[current];
+ current := current + 1
+ }
+
+}
+
--
GitLab