1 theory TimeLimit

     2 imports Base

     3 begin

     4 

     5 section {* Restricting the Runtime of a Function *} 

     6 

     7 

     8 text {*

     9   {\bf Problem:}

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

    11 

    12   {\bf Solution:} This can be achieved using time limits.\smallskip

    13 

    14   Assume the following function should run only five seconds:

    15 

    16   *}

    17 

    18 ML {*

    19 fun ackermann (0, n) = n + 1

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

    21   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))

    22 *}

    23 

    24 ML {* ackermann (3, 12) *}

    25 

    26 (* takes more than 10 seconds *)

    27 

    28 text {*

    29   The call can be encapsulated in a time limit of five seconds as follows:

    30   *}

    31 

    32 ML {* 

    33 TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (3, 12) 

    34   handle TimeOut => ~1

    35 *}

    36 

    37 text {*

    38   The function "TimeLimit.timeLimit" has type "???" and is defined in

    39   TODO: refer to code *}

    40 

    41 end