Examples/python/contract/example.i


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

/* File : example.i */
%module example

%contract gcd(int x, int y) {
require:
	x >= 0;
	y >= 0;
}

%contract fact(int n) {
require:
	n >= 0;
ensure:
	fact >= 1;
}

%inline %{
extern int    gcd(int x, int y);
extern int    fact(int n);
extern double Foo;
%}