theory TimeLimit

imports "../Appendix"

begin

section {* Restricting the Runtime of a Function\label{rec:timeout} *} 

text {*

  {\bf Problem:}

  Your tool should run only a specified amount of time.\smallskip

  Assume you defined the Ackermann function on the ML-level.

*}

ML %grayML{*fun ackermann (0, n) = n + 1

  | ackermann (m, 0) = ackermann (m - 1, 1)

  | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}

text {*

  Now the call 

  @{ML_response_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"}

  takes a bit of time before it finishes. To avoid this, the call can be encapsulated 

  in a time limit of five seconds. For this you have to write

@{ML_response_fake_both [display,gray]

"~1"}

  where @{text TimeOut} is the exception raised when the time limit

  is reached.

  or later, because this version of PolyML has the infrastructure for multithreaded 

\begin{readmore}

\end{readmore}

*}

end