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