blob: b4244b8d240041166c85cb24666e16f92c70f9a8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
// RUN: %boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// McCarthy 91 function
procedure F(n: int) returns (r: int)
ensures 100 < n ==> r == n - 10;
ensures n <= 100 ==> r == 91;
{
if (100 < n) {
r := n - 10;
} else {
call r := F(n + 11);
call r := F(r);
}
}
|
