1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
// BoogiePL Examples
type real;
type elements;
var x:int; var y:real; var z:ref; // Variables
var x.3:bool; var $ar:ref; // Names can have glyphs
const a, b, c:int; // Consts
function f (int, int) returns (int); // Function with arity 2
function g ( int , int) returns (int); // Function with arity 2
function h(int,int) returns (int); // Function with arity 2
function m (int) returns (int); // Function with arity 1
function k(int) returns (int); // Function with arity 1
axiom
(forall x : int :: f(g(h(a,b),c),x) > 100) ;
procedure p (x:int, y:ref) returns (z:int, w:[int,ref]ref, q:int);
procedure q(x:int, y:ref) returns (z:int) // Procedure with output params
requires x > 0; // as many req/ens/mod you want
ensures z > 3;
ensures old(x) == 1; // old only in ensures..
modifies z,y,$ar;
{
var t, s: int;
var r: [int,ref]ref;
start: // one label per block
t := x;
s := t;
z := x + t;
call s, r,z := p(t,r[3,null]); // procedure call with mutiple returns
goto continue, end ; // as many labels as you like
continue:
return; // ends control flow
end:
goto start;
}
procedure s(e: elements) { L: return; }
procedure r (x:int, y:ref) returns (z:int);
type ref;
const null : ref;
|
