Skip to content
Snippets Groups Projects
Commit 55e161b6 authored by Bart Wijgers's avatar Bart Wijgers
Browse files

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).
parent b2bf15c6
No related branches found
No related tags found
No related merge requests found
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
}
......@@ -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
}
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
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment