CSE 321 Homework 2

Consider the Sort operation specified here (if s and t are strings of items, s is substring of t if and only if there exist strings of items a and b such that t = a * s * b):

    /*!
        math operation IS_ORDERED (
                s: string of integer
            ): boolean is
            for all u, v: integer
                    where (<u> * <v> is substring of s)
                (u <= v)
    !*/

    global_procedure Sort (
            alters Queue_Of_Integer& q
        );
    /*!
        ensures
            q is permutation of #q  and
            IS_ORDERED (q)
    !*/

1. Here is an implementation of the Sort operation using the insertion sort algorithm:

       procedure_body Sort (
               alters Queue_Of_Integer& q
           )
       {
           object Queue_Of_Integer tmp;
           while (q.Length () > 0)
           {
               object Integer x;
               q.Dequeue (x);
               Insert_In_Order (tmp, x);
           }
           q &= tmp;
       }
   

   Provide an implementation for the Insert_In_Order global procedure specified below.

    global_procedure Insert_In_Order (
            alters Queue_Of_Integer& q,
            consumes Integer& x
        );
    /*!
        requires
            IS_ORDERED (q)
        ensures
            q is permutation of #q * <#x>  and
            IS_ORDERED (q)
    !*/

2. Assume that operations Split and Merge specified below are given. Provide an implementation of the Sort operation using the mergesort algorithm and using the Split and Merge operations.

    global_procedure Split (
            consumes Queue_Of_Integer& q,
            produces Queue_Of_Integer& q1,
            produces Queue_Of_Integer& q2
        );
    /*!
        ensures
            q1 * q2 is permutation of #q  and
            |q2| <= |q1| <= |q2| + 1
    !*/

    global_procedure Merge (
            consumes Queue_Of_Integer& q1,
            consumes Queue_Of_Integer& q2,
            produces Queue_Of_Integer& q
        );
    /*!
        requires
            IS_ORDERED (q1)  and  IS_ORDERED (q2)
        ensures
            q is permutation of #q1 * #q2 and
            IS_ORDERED (q)
    !*/