级别: 中级

            int factorial(int n)
            {
            return n * factorial(n - 1);
            }
            

            int factorial(int n)
            {
            if(n == 1)
            {
            return 1;
            }
            else
            {
            return n * factorial(n - 1);
            }
            }
            

            function sum_list(list l)
            is l null?
            yes - the sum of an empty list is 0 - return that
            data = head of list l
            rest_of_list = rest of list l
            the sum of the list is:
            data + sum_list(rest_of_list)
            

            (define sum-list (lambda (l)
            (if (null? l)
            0
            (let (
            (data (car l))
            (rest-of-list (cdr l)))
            (+ data (sum-list rest-of-list))))))
            

            int sum_list(struct list_node *l)
            {
            if(l == NULL)
            return 0;
            return l.data + sum_list(l.next);
            }
            

            (define is-in-list
            (lambda   (the-list the-string)
            ;;Check for base case of "list empty"
            (if (null? the-list)
            #f
            ;;Check for base case of "found item"
            (if (equal? the-string (car the-list))
            #t
            ;;Run the algorithm on a smaller problem
            (is-in-list (cdr the-list) the-string)))))
            

            (define is-in-list2
            (lambda (the-list the-string)
            (letrec
            (
            (recurse (lambda (internal-list)
            (if (null? internal-list)
            #f
            (if (equal? the-string (car internal-list))
            #t
            (recurse (cdr internal-list)))))))
            (recurse the-list))))
            

            (define is-in-list2
            (lambda (the-list the-string)
            ;;Named Let
            ;;This let block defines a function called "recurse" that is the
            ;;body of this let.  The function's parameters are the same as
            ;;the variables listed in the let.
            (let recurse
            ;;internal-list is the first and only parameter.  The
            ;;first time through the block it will be primed with
            ;;"the-list" and subsequent calls to "recurse" will
            ;;give it whatever value is passed to "recurse"
            ( (internal-list the-list) )
            ;;Body of function/named let block
            (if (null? internal-list)
            #f
            (if (equal? the-string (car internal-list))
            #t
            ;;Call recursive function with the
            ;;rest of the list
            (recurse (cdr internal-list)))))))
            

            (define is-ascending
            (lambda (the-list)
            ;;First, Initialize the algorithm.  To do this we
            ;;need to get the first value, if it exists, and
            ;;use it as a seed to the recursive function
            (if (null? the-list)
            #t
            (let is-ascending-recurse
            (
            (previous-item (car the-list))
            (remaining-items (cdr the-list))
            )
            ;;Base case #1 - end of list
            (if (null? remaining-items)
            #t
            (if (< previous-item (car remaining-items))
            ;;Recursive case, check the rest of the list
            (is-ascending-recurse (car remaining-items) (cdr remaining-items))
            ;;Base case #2 - not in ascending order
            #f))))))
            

            void print_report(struct report_line *report_lines, int num_lines)
            {
            int num_lines_this_page = 0;
            int page_number = 1;
            int current_line; /* iterates through the lines */
            int current_group = 0; /* tells which grouping we are in */
            int previous_group = 0; /* tells which grouping was here on the last loop */
            int group_total = 0; /* saves totals for printout at the end of the grouping */
            print_headings(page_number);
            for(current_line = 0; current_line < num_lines; current_line++)
            {
            num_lines_this_page++;
            if(num_lines_this_page == LINES_PER_PAGE)
            {
            page_number++;
            page_break();
            print_headings(page_number);
            }
            current_group = get_group(report_lines[current_line]);
            if(current_group != previous_group)
            {
            print_totals_for_group(group_total);
            group_total = 0;
            }
            print_line(report_lines[current_line]);
            group_total += get_line_amount(report_lines[current_line]);
            }
            }
            

            void print_report(struct report_line *report_lines, int num_lines)
            {
            int num_lines_this_page = 0;
            int page_number = 1;
            int current_line; /* iterates through the lines */
            int current_group = 0; /* tells which grouping we are in */
            int previous_group = 0; /* tells which grouping was here on the last loop */
            int group_total = 0; /* saves totals for printout at the end of the grouping */
            /* initialize */
            print_headings(page_number);
            /* Seed the values */
            print_report_i(report_lines, 0, 1, 1, 0, 0, num_lines);
            }
            void print_report_i(struct report_line *report_lines, /* our structure */
            int current_line, /* current index into structure */
            int num_lines_this_page, /* number of lines we've filled this page */
            int page_number,
            int previous_group, /* used to know when to print totals */
            int group_total, /* current aggregated total */
            int num_lines) /* the total number of lines in the structure */
            {
            if(current_line == num_lines)
            {
            return;
            }
            else
            {
            if(num_lines_this_page == LINES_PER_PAGE)
            {
            page_break();
            print_headings(page_number + 1);
            print_report_i(
            report_lines,
            current_line,
            1,
            page_number + 1,
            previous_group,
            group_total,
            num_lines);
            }
            else
            {
            int current_group = get_group(report_lines[current_line]);
            if(current_group != previous_group && previous_group != 0)
            {
            print_totals_for_group(group_total);
            print_report_i(
            report_lines,
            current_line,
            num_lines_this_page + 1,
            page_number,
            current_group,
            0,
            num_lines);
            }
            else
            {
            print_line(report_lines[current_line]);
            print_report_i(
            report_lines,
            current_line + 1,
            num_lines_this_page + 1,
            page_number,
            current_group,
            group_total + get_line_amount(report_lines[current_line]),
            num_lines);
            }
            }
            }
            }
            

只有当 current_line 的当前值与 current_line 的先前值不同时，R2 才会发生，因为 current_group 和 previous_group 直接由它派生而来。

只有 num_lines_this_page 中的变化会令 R1 发生，而这种变化只能由 R2 和 R3 产生。

由于只有以 R3 为基础才能发生 R2，且只有以 R2 和 R3 为基础才能发生 R1，我们可以断定，current_line 必须是增加的，而且只能是单调递增。

因此，如果 current_line 的某一值可以终止，那么 current_line 之前的所有值都可以终止。

通过确认每一个打印一行的过程都相应使 num_lines_this_page 增 1，条件 2 能得到确定。在以下三种情况下完成行打印：

1. 打印组的总数。
2. 打印单个的报告行。
3. 打印页眉。

观察可见，行打印条件 1 和 2 将 num_lines_this_page 增 1，行打印条件 3 在一个 分页/页眉 组合打印之后将 num_lines_this_page 重新设置为适当的值（常规的条件 3）。定理 1 的要求得到了满足，所以我们就已经证明了程序会在打印 LINES_PER_PAGE 行之后进行一次分页。

通过归纳可以证明条件 2 和 3，并且，实际上这只是第一个终止证明的重复。我们可以使用终止的证明来最终证明条件 3。基于那个证明，以及 current_line 从 0 开始的假定，条件 2 为真。因此，我们已经证明报告的每一行都严格只打印一次。

            int test1()
            {
            int a = 3;
            test1(); /* recursive, but not a tail call.  We continue */
            /* processing in the function after it returns. */
            a = a + 4;
            return a;
            }
            int test2()
            {
            int q = 4;
            q = q + 5;
            return q + test1(); /* test1() is not in tail position.
            * There is still more work to be
            * done after test1() returns (like
            * adding q to the result
            */
            }
            int test3()
            {
            int b = 5;
            b = b + 2;
            return test1();  /* This is a tail-call.  The return value
            * of test1() is used as the return value
            * for this function.
            */
            }
            int test4()
            {
            test3(); /* not in tail position */
            test3(); /* not in tail position */
            return test3(); /* in tail position */
            }
            

            ;;Unoptimized tail-call
            my_function:
            ...
            ...
            ;PUSH ARGUMENTS FOR the_function HERE
            call the_function
            ;results are already in %eax so we can just return
            movl %ebp, %esp
            popl %ebp
            ret
            ;;Optimized tail-call optimized_function:
            ...
            ...
            ;save the old return address
            movl 4(%ebp), %eax
            ;save old %ebp
            movl (%ebp), %ecx
            ;Clear stack activation record (assuming no unknowns like
            ;variable-size argument lists)
            addl $(SIZE_OF_PARAMETERS + 8), %ebp ;(8 is old %ebp + return address))
            ;restore the stack to where it was before the function call
            movl %ebp, %esp
            ;Push arguments onto the stack here
            ;push return address
            pushl %eax
            ;set ebp to old ebp
            movl %ecx, %ebp
            ;Execute the function
            jmp the_function