diff --git a/examples/abs b/examples/abs index 85e39d7a724b857d1e70fd28cd3ace646264ba85..6830938ed4ad569fd434e2aefc6414cd48ed2a54 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 624fa1495f47a2378ffaa1f63815a9c0e8fd9151..d137deb56db189cf33abac9756701d2fd31f4eb4 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 0000000000000000000000000000000000000000..607323c4c4bdea8c74b52599d4651346eafe8a19 --- /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 + } + +} +