equal
deleted
inserted
replaced
1 theory TimeLimit |
1 theory TimeLimit |
2 imports "../Base" |
2 imports "../Base" |
3 begin |
3 begin |
4 |
4 |
5 section {* Restricting the Runtime of a Function *} |
5 section {* Restricting the Runtime of a Function\label{rec:timeout} *} |
6 |
6 |
7 text {* |
7 text {* |
8 {\bf Problem:} |
8 {\bf Problem:} |
9 Your tool should run only a specified amount of time.\smallskip |
9 Your tool should run only a specified amount of time.\smallskip |
10 |
10 |
28 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
28 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
29 in a time limit of five seconds. For this you have to write: |
29 in a time limit of five seconds. For this you have to write: |
30 |
30 |
31 @{ML_response [display,gray] |
31 @{ML_response [display,gray] |
32 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) |
32 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) |
33 handle TimeOut => ~1" |
33 handle TimeLimit.TimeOut => ~1" |
34 "~1"} |
34 "~1"} |
35 |
35 |
36 where @{ML_text TimeOut} is the exception raised when the time limit |
36 where @{ML_text TimeOut} is the exception raised when the time limit |
37 is reached. |
37 is reached. |
38 |
38 |