CSE 221 Closed Lab 8 Warm-Up Exercise

Write the bodies for the global operations Display_Width and Load_Naturals shown below. Review your code carefully and trace it on some examples, but do not enter it into the computer until closed lab. The objective is to have code that works the first time you type it in (except perhaps for typos).

Informally, when Load_Naturals is called, the input stream input is open to a file that contains a sequence of natural numbers, one number per line. Load_Naturals gets these natural numbers and puts them into a sequence object named s. While doing this, Load_Naturals also determines the maximum number of display spaces that would be necessary to display any one of the input natural numbers, where the display will include commas, as in the previous closed-lab assignment. This number is the outgoing value of the Integer object max_display_width. For example, the display width for 87654321 is 10, as in 87,654,321.

Since two students share a workstation during closed lab, if you want to you may work with a partner on this homework exercise. If you do work with a partner, you need only turn in one solution for this homework. Be sure to put the names of both students on the solution that is turned in.

/*!
    math operation NUMBER_OF_DIGITS (
            n: NATURAL_MODEL
        ): integer
        implicit definition
            if n < 10
            then NUMBER_OF_DIGITS(n) = 1
            else NUMBER_OF_DIGITS(n) = 1 + NUMBER_OF_DIGITS(n DIV 10)

    math operation DISPLAY_WIDTH (
            n: NATURAL_MODEL
        ): integer
        implicit definition
            if n  < 10
            then DISPLAY_WIDTH(n) = 1
            else DISPLAY_WIDTH(n) = NUMBER_OF_DIGITS(n) + 
                                    ((NUMBER_OF_DIGITS(n) - 1) DIV 3)
!*/



global_function Integer Display_Width (
        preserves Natural_Put_To_With_Commas_1& n
    );
    /*!
        ensures
            Display_Width = DISPLAY_WIDTH(n)
            
    !*/


global_procedure Load_Naturals (
        alters   Character_IStream& input,
        produces Sequence_of_Naturals& s,
        produces Integer& max_display_width
    );
    /*!
        requires
            input.is_open = true and
            input.content = [a sequence of one or more natural number values, 
                            one per line, as in
                            n0'\n'
                            n1'\n'
                            ...
                            nk'\n']
        ensures
            input.is_open = true and
            input.ext_name = #input.ext_name and
            input.content = empty_string and
            [s = <n0,n1,n2, ..., nk> and
            max_display_width = maximum of {DISPLAY_WIDTH(n0),DISPLAY_WIDTH(n1), 
                                            ..., DISPLAY_WIDTH(nk)}]
            
    !*/