source:
CIVL/examples/languageFeatures/bigO.cvl@
4f22a92
| Last change on this file since 4f22a92 was ef21fe4, checked in by , 12 years ago | |
|---|---|
|
|
| File size: 278 bytes | |
| Rev | Line | |
|---|---|---|
| [8fa5a7b] | 1 | #include<civlc.h> |
| [ef21fe4] | 2 | $input double y; |
| [8fa5a7b] | 3 | |
| 4 | void main() { | |
| [ef21fe4] | 5 | $assume y > 10; |
| 6 | $assume $forall {int i | i > 0} $forall {double x | x > 0} i*x == $O(x); | |
| 7 | $assume $forall {double z | z > 0} z*$O(z) == $O(z*z); | |
| 8 | $assert 6.0 == $O(1); | |
| 9 | $assert 3*y == $O(y); | |
| 10 | $assert 3*y*y == $O(y*y); | |
| [8fa5a7b] | 11 | } |
Note:
See TracBrowser
for help on using the repository browser.
