source:
CIVL/examples/experimental/contract.cvl@
e0fc189
| Last change on this file since e0fc189 was 8fa5a7b, checked in by , 13 years ago | |
|---|---|
|
|
| File size: 202 bytes | |
| Rev | Line | |
|---|---|---|
| [f28d814] | 1 | #include<civlc.h> |
| [59b5362] | 2 | |
| 3 | double f(double x) | |
| [f28d814] | 4 | $requires x > 0; |
| 5 | $ensures $true; | |
| [59b5362] | 6 | ; |
| 7 | ||
| 8 | double g(double x) | |
| [f28d814] | 9 | $requires x > 0; |
| 10 | $ensures $result >= 0; | |
| [59b5362] | 11 | { |
| 12 | return g(x)*g(x); | |
| 13 | } | |
| 14 | ||
| 15 | double main() { | |
| 16 | return g(2); | |
| 17 | } |
Note:
See TracBrowser
for help on using the repository browser.
