1 theory TimeLimit |
1 theory TimeLimit |
2 imports "../Appendix" |
2 imports "../Appendix" |
3 begin |
3 begin |
4 |
4 |
5 section {* Restricting the Runtime of a Function\label{rec:timeout} *} |
5 section \<open>Restricting the Runtime of a Function\label{rec:timeout}\<close> |
6 text {* |
6 text \<open> |
7 {\bf Problem:} |
7 {\bf Problem:} |
8 Your tool should run only a specified amount of time.\smallskip |
8 Your tool should run only a specified amount of time.\smallskip |
9 |
9 |
10 {\bf Solution:} In Isabelle 2016-1 and later, this can be achieved |
10 {\bf Solution:} In Isabelle 2016-1 and later, this can be achieved |
11 using the function @{ML apply in Timeout}.\smallskip |
11 using the function @{ML apply in Timeout}.\smallskip |
12 |
12 |
13 Assume you defined the Ackermann function on the ML-level. |
13 Assume you defined the Ackermann function on the ML-level. |
14 *} |
14 \<close> |
15 |
15 |
16 ML %grayML{*fun ackermann (0, n) = n + 1 |
16 ML %grayML\<open>fun ackermann (0, n) = n + 1 |
17 | ackermann (m, 0) = ackermann (m - 1, 1) |
17 | ackermann (m, 0) = ackermann (m - 1, 1) |
18 | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *} |
18 | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))\<close> |
19 |
19 |
20 text {* |
20 text \<open> |
21 |
21 |
22 Now the call |
22 Now the call |
23 |
23 |
24 @{ML_response_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"} |
24 @{ML_response_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"} |
25 |
25 |
29 @{ML_response_fake_both [display,gray] |
29 @{ML_response_fake_both [display,gray] |
30 "Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) |
30 "Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) |
31 handle TIMEOUT => ~1" |
31 handle TIMEOUT => ~1" |
32 "~1"} |
32 "~1"} |
33 |
33 |
34 where @{text TimeOut} is the exception raised when the time limit |
34 where \<open>TimeOut\<close> is the exception raised when the time limit |
35 is reached. |
35 is reached. |
36 |
36 |
37 Note that @{ML "apply" in Timeout} is only meaningful when you use PolyML 5.2.1 |
37 Note that @{ML "apply" in Timeout} is only meaningful when you use PolyML 5.2.1 |
38 or later, because this version of PolyML has the infrastructure for multithreaded |
38 or later, because this version of PolyML has the infrastructure for multithreaded |
39 programming on which @{ML "apply" in Timeout} relies. |
39 programming on which @{ML "apply" in Timeout} relies. |